I’ve been trying to talk to people about this stuff for a long time. This will mostly be about what’s gotten results with a number of people who at least wanted to learn more. That might help you out with you having some stuff that works well to start with plus avoiding what might not.
“Looked at from the right angle this is already enough justification for utilizing more formal methods in other parts of the software development stack because parsing is a fundamental part of the programming toolkit and a pretty big success in terms of utility.”
Most want a library or automation of repetitive stuff. Obvious counter-argument is that this means people should use parser generators to get it done quickly/correctly and/or make better ones. Not start doing formal methods to cover parsing.
“I think most programmers are also familiar with or have heard of type systems. “
Well, they get simple, type systems but not like type theory or anything. This is a way to lure them in, though. I tell them that tests prove correctness for specific inputs. Whereas, types with input validation lets the type checker show the numbers, strings, objects, etc will always be assigned or used correctly (far as type system covers) no matter what the inputs. Then, I say both advanced, type systems and formal verification can do that for more attributes of their program with examples like overflows, race freedom, and so on. Programmers see value in that.
Whereas, many folks start throwing out examples of advanced stuff in Coq, etc that nobody understands built on concepts like recursion they’re weak on. I think it might be better to get them into functional programming with SML, Ocaml, or Haskell first. Tell them about benefits like easier modifications and concurrency from functional style. Plus, how they will learn to think in new ways they can apply in existing languages. They learn that stuff running into advanced typing from a functional style where it makes more sense. Then, you can tell them formal verification is like that except covering even more properties. Kind of arbitrary where they create their own type systems to do what they need. They might see more value in it. If not, they learned functional programming. :)
“The categories I’m familiar with are theorem proving and verified programming”
Verified programming is programming + theorem proving, or theorem proving about source code. The distinction most papers make is whether they manually use a proof assistant or have an automated solver. Most of the languages that feed verification conditions into automated solvers have some they can’t handle. Then, they use proof assistants on them. So, there’s hybrids I say are “mostly automated for the kinds of things they can handle.” Then, I say they’ll need a proof engineer for the rest, convert them to runtime checks, or just do nothing while fuzzing the heck out of that component. They like easy options. I give them easy options.
“abstract interpretation as a general technique of program approximation and analysis (Astrée, Polyspace, Verasco, K framework, etc.)”
I tell people there are “push-button tools” that create models of the program, cover specific properties like “no overflows,” and can automatically find problems or show there probably aren’t any. I add false positives can be big for some of them but some like RV-Match have few to none. Emphasizing they need no knowledge of formal methods to use them is always well-received. Some people might also want to work on these tools as their formal methods projects. I tell them that’s high-impact and most useful, but also hard work on realistic, messy languages. There’s also established tooling they can build on. I want them knowing what they’re getting into ahead of time.
“By using a more precise/formal language to describe requirements we can uncover implicit assumptions and inconsistencies before investing time and effort into an implementation that will inevitably run into a dead end because of an inconsistency in our understanding. “
“We can avoid the hassle of building a prototype and throwing it away by specifying and validating a formal model of what we’re trying to implement ahead of the actual implementation process.”
Actually, most programming starts with prototyping to build an understanding that drives creating something that works. Probably why Smalltalk was both highly productive and low defect in what studies I saw. For Brute-Force Assurance, I was leaning toward pushing something with Smalltalk-like, incremental development to let them experiment until they figure out the specification they’re looking for. Then, they annotate Strongtalk- and SPARK-style with the specs/types to begin the Correct-by-Construction-style development. New pieces are done similarly. Starting with specs or proofs hasn’t been shown empirically to be better than that yet. If they already exist and are validated, then by all means proceed right to spec-to-code flow.
“I think the easiest places to start applying formal methods are in operational contexts. Software doesn’t exist in a vacuum.”
I like that you’re doing these examples. Yours are different from others I see. That’s great. I’m still pushing everyone to do Design-by-Contract, contract/property-based testing, and/or program analyzers as the start since they’re most applicable with least knowledge required. Also, people keep adding contracts and PBT to more languages. If DbC, mention the benefits of contracts, that tests can be generated from them, and that they can become runtime checks for fuzzers and/or deployment to take you right to the problem. At the least, they can do preconditions on the initial inputs to make sure they have the expected properties. Will save people so much time. All they gotta know is boolean for the range errors.
“There are many successful projects like seL4 microkernel, CompCert’s verified C compiler, and Project Everest from Microsoft.”
These are great examples given they’re reusable in many other projects. Two won’t change much either. That’s best use of formal methods given the rare expertise and costs they come with.
These are good points. I forgot about contracts and will include them in the presentation I’m working on for our next formal methods meeting.
Re: examples. I think people overthink applications of formal methods. Alloy is easy to pick up and apply and the return on investment (subjectively) feels extremely high. Even just trying to come up with a model clears up a lot of confusion.
“I forgot about contracts and will include them in the presentation I’m working on for our next formal methods meeting.”
Awesome! Here’s you a reference that has info good for both programmers and project managers. Got it from hwayne.
“Alloy is easy to pick up and apply and the return on investment (subjectively) feels extremely high. “
Hey, keep exploring and writing up what you figure out. Your posts have all been interesting since you seem to think about and use it differently than a lot of folks. Who knows what you’ll find! :)
Does your website have an RSS/Atom feed?
Not yet but it’s on my list of things to add.