Why Don't People Use Formal Methods?
Skip to Content
New: Logic for Programmers is out in print! Learn more and buy it here..
Hillel Wayne
Posted on<br>Jan 21, 2019
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 , 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...