Why Don't People Use Formal Methods?

I saw this question on the Software Engineering Stack Exchange: What are the barriers that prevent widespread adoption of formal methods? The question was closed as opinion-based, and most of the answers were things like “its too expensive!!!” or “website isn’t airplane!!!” These are sorta kinda true but don’t explain very much. I wrote this to provide a larger historical picture of formal methods, why they’re actually so unused, and what we’re doing to make them used. Before we begin, we need to lay down some terms. There really isn’t a formal methods community so much as a few tiny bands foraging in the Steppe.1 This means different groups use terms in different ways. Very broadly, there are two domains in FM: formal specification is the study of how we write precise, unambiguous specifications, and formal verification is the study of how we prove things are correct. But “things” includes both code and abstract systems. Not only do we use separate means of specifying both things, we often use different means to verify them, too. To make things even more confusing, if somebody says they do formal specification, they usually mean they both specify and verify systems, and if somebody says they do formal verification, they usually mean mean they both specify and verify code. For clarity purposes, I will divide verification into code verification (CV) and design verification (DV), and similarly divide specification into CS and DS. These are not terms used in the wider FM world. We’ll start by talking about CS and CV, then move on to DS and DV. Additionally, we can do partial verification, where we only verify a subset of the spec, or full verification, where we verify the entire spec. This could be the difference between proving “it never crashes or accepts the wrong password” or “it never crashes or admits the wrong password and locks the account if you give the wrong password three times.” Most of this history will assume we’re doing full verification. We should also clarify the type of software we’re formalizing. Most people implicitly divide software into high-assurance software, such as medical devices and aircraft, and everything else. People assume that formal methods are widely used in the former and unnecessary for the latter. This, if anything, is too optimistic: most people in high-assurance software don’t use formal methods. We’ll focus instead on “regular” software. Finally, a disclaimer: I am not a historian, and while I tried to do my due diligence there are probably mistakes here. Also, I specialize in formal specification (DS and DV), so there are more likely to be mistakes in anything I say about code verification. If you see something wrong, email me and I’ll fix it.2 Formal Coding Getting the Spec Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification, or spec, for what the code should do, one where we can unambiguously say whether a specific output follows the spec. Just saying a list is “sorted” is unclear: we don’t know what we’re sorting, what criteria we’re using, or even what we mean by “sort”. Instead, we might say “A list of integers l is sorted in ascending order if for any two indices i and j, if i < j, then l[i] <= l[j]”. Code specs fall into three major camps: The first is writing them as statements independent of the code. We would write our sort function, and in a separate file write the theorem “this returns sorted lists”. This is the oldest form of spec and is still the way Isabelle and ACL2 do things.3 The second embeds specs in the code in the form of pre/postconditions, assertions, and invariants. We might add a postcondition on the function that “the return value is a sorted list”. Assertion-based specs were originally formalized as Hoare Logic and were first integrated into a programming language with Euclid in the early 1970s.4 This style is also called Design by Contract and is the most popular form of industrial verification.5 Finally, we have type systems. By Curry-Howard correspondence, any math theorem or proof can be encoded as a dependent type. We’d define the type of “sorted lists” and declare our function has the type signature [Int] -> Sorted [Int]. You can see examples of how all of these look at Let’s Prove Leftpad. HOL4 and Isabelle are good examples of “independent theorem” specs, SPARK and Dafny have “embedded assertion” specs, and Coq and Agda have “dependent type” specs.6 If you squint a bit it looks like these three forms of code spec map to the three main domains of automated correctness checking: tests, contracts, and types. This is not a coincidence. Correctness is a spectrum, and formal verification is one extreme of that spectrum. As we reduce the rigour (and effort) of our verification we get simpler and narrower checks, whether that means limiting the explored state space, using weaker types, or pushing verification to the runtime. Any means of total specification then becomes a means of partial specification, and vice versa: many consider Cleanroom a formal verification technique, which primarily works by pushing code review far beyond what’s humanly possible. “What’s the right spec?” Verification proves code matches its spec. This raises a question: how do we know we have the right spec? Finding the right spec is one of the biggest challenges in formal methods. It’s also one of the most raised objections, but the way skeptics mean it isn’t exactly the same as the way advocates think of it. When outsiders say “how do you have the right spec?” they’re usually thinking of validation: showing a spec actually does what the client wants. If you formally prove your code sorts a list, but the customer actually wants Uber For Soups ™, you’ve just wasted a bunch of time. Only by rapid iteration and short feedback cycles, people argue, can you actually validate your requirements. It is true that verifying code does not validate the code. There are two problems with this argument, though. The first is that it just delays the value of FM, not eliminate it entirely. Once you’ve done your rapid iterations, you presumably have an idea of what your customer wants. Then you start verifying code. Second, while we don’t know what exactly the customer wants, there are some things we can assume they don’t want. They don’t want the software randomly crashing on them. They don’t want security holes. Everybody recognizes the importance of this: after all, nobody is saying you should skip unit tests while you iterate. So, at the very least, prove your version control system doesn’t randomly delete chapters of a user’s book.7 The problem with finding the right spec is more fundamental: we often don’t know what we want the spec to be. We think of our requirements in human terms, not mathematical terms. If I say “this should distinguish parks from birds”, what am I saying? I could explain to a human by giving a bunch of pictures of parks and birds, but that’s just specific examples, not capturing the idea of distinguishing parks from birds. To actually translate that to a formal spec requires us to be able to formalize human concepts, and that is a serious challenge. Don’t get me wrong, it’s possible to figure out the appropriate specs here and experts do it all of the time. But writing appropriate specs is a skill you need to develop, just as you needed to develop coding skills. This is why a lot of the more recent successes with code verification have been things with an obvious map between what we want and what we can express we want. For example, CompCert is a formally verified C compiler. The spec there is “this will never miscompile”. And none of this is the actual verification part. Once you have a spec, you still need to prove the code matches the spec. Proving the Spec The earliest means of code verification we see is the the Dijkstra-style “think really hard about why it’s true” method, which is basically what ALGOL was designed to help do. For example, I might “prove” an insertion sort works by arguing Base Case: if we have an empty list and add one element to it, that will be the only element, so it will be sorted. If we have a sorted list with k elements and add one element, we insert the element so that it is after all smaller numbers and before all larger numbers. This means the list is still sorted. By induction, insert sort will sort the entire list. Obviously it’d look more rigorous than that, but that’s the general idea. Dijkstra and others used this style to prove a bunch of algorithms were correct, including many concurrency primitives. It’s also the style that gives rise to the Knuth quote “Beware of bugs in the above code; I have only proved it correct, not tried it.” It’s pretty easy to screw up a math proof in a way nobody notices, and I’ve read estimates that something like 20% of published math proofs have errors in them. Peter Guttmann has a great essay on how farcical code proofs got, where tons of “proven” code would immediately crash if run. At the same time we were exploring how to automatically prove mathematical theorems, the first such theorem prover coming out in 1967. Researchers in the Pascal community were using theorem provers to verify programs by the early 1970s, then programming in dedicated verification languages by mid-decade. People would write some properties of the code and then write a checkable proof that the code had those properties. Earlier theorem provers simply helped humans check and verify proofs while more sophisticated ones could prove parts of the theorem on their own. Which leads to the next problem. Proofs are hard Proofs are hard. Obnoxiously hard. “Quit programming and join the circus” hard. Surprisingly, formal code proofs are often more rigorous than the proofs most mathematicians write! Mathematics is a very creative activity with a definite answer that’s only valid if you show your work. Creativity, formalism, and computers are a bad