GoKawiilI 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. 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.
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:
... continue reading