What works (and doesn't) selling formal methods

> For example, the formal proofs of the seL4 kernel establish amongst other things that the implementation C code precisely matches an abstract model of the kernel. This is a really powerful and impressive result, but to understand it, you have to study the formal model in detail.

No not the complexity of understanding the abstract model - the fact that you have agree with the abstract model, the fact that the abstract model has to be a good abstract model of your system. This is what everyone says about TLA+, that sure you can prove a raft spec has no deadlock but you can't extract an implementation from the same spec. Yes I know some proof systems do actually let you extract (fsharp) but they are few and far between because proof languages are to programming languages as the NBA is to college ball: a whole different league of precision/specification (so lots of things cannot be translated).

I don't have answer/solution. Not saying that I do. The article is good though, reads like any basic sales journey (which isn't a bad thing).

Model checking, for example, is not as hard as it sounds and not nearly as expensive or time consuming as building the wrong thing. Most programmers I’ve taught don’t seem to have too much difficulty learning TLA+ or Alloy. The concepts themselves are fundamentally rather simple.

Theorem proving does take some expertise. But it’s also not an insurmountable obstacle.

However I agree that there’s a spectrum of cost and the higher you go down the assurance chain the effort and time it will take. Often we do price in the cost of errors into the holistic process of software (eg: SRE style error budgets, iterative development, etc).

One angle that works for me when deciding when to use a more substantial FM is the cost of getting it wrong (or conversely, how important is it that we get some key thing right)?

If I’m building a financial database can my business afford to lose customers’ money? Do we have that liability built into our insurance?

Sometimes you need to go slow at first in order to go fast later.

And some properties are simply too hard to trust to some boxes and arrows and a prayer.

I can see the intellectual appeal and even the argument for formalism in some high-risk areas. I guess I am most burnt by the advent of hyperlinted, theatrically "typechecked" enterprise Python. I don't think people pushing this stuff would have the balls to introduce an actually formal environment, since even Java is there, not to mention ML-style languages, Rust etc. Maybe there's fear about the staffing and scary appearance, which the article also mentions. (I still sincerely wait for a bigger niche for functional and lispy shops, maybe when the industry transforms with de-monopolization.)

But there is a common thread in the bad kind of arguing for formalisms, where the Scotsmen are never true and your lazy human mind isn't Godlike enough to reason about the program correctly from the start. I actually like how TFA moves toward communicating better so maybe conversations could be more productive in these aspects.

For example, deployment software. There's probably some way to formally model deployment. But most deployment software in the wild is written like, "here are 100 things that can go wrong while you're deploying, and 100 corresponding business rules for what to do."

I do sometimes fantasize about a more pure-Computer-Science world where all text formats are a formally-defined grammar, all systems are state machines, and everything has a spec ;-)

I would have loved to have a formal specification of this, not just to have my code checked, but also to make sure the specification is coherent.

The problems with that were:

- The cost of creating that specification would have been very substantial, both in money and in time.

- The end to end functionality of the system was verified anyway and could not have been replaced by a formal correctness proof. Creating a few more test cases is cheap, creating a formal verification is extremely hard. Tye regulator expects that verification, it does not expect a formal proof. This is actually a project risk.

- The people writing the specification do not think formally, they concern themselves with overall functionality, which they them translated into a more detailed description. There is a serious communication problem here if you want formal verification.

I really like the concept, but to apply it you need to integrate it from ground up and rethink how you write software.

IMO, I see FMs as converging to be part of the type system that is checked by the compiler automatically during CICD.

If it’s not, it’s adoption cost is too high 90% of the time.

The only things that gets widely adopted follow that idea: types, unit tests, properties, fuzzing, integration test, simulation, packaging in a deployment pipeline, etc.

Finally, knowing that incompleteness theorems are a thing, formal methods will always fall short in some fundamental way.

Let me explain this in formal methods terms.

As programs grow their state space naturally exponentially expands. One of the major methods of formal methods is to contain that growth but even then it's exponential by its nature. Unconstrained programs written normally have vast, vast state spaces. It takes very little before human beings fundamentally can not know what all is lurking in the state space of a program.

A formal methods advocate sees that exponential state space and is well aware of the dragons lurking within the vast majority of programs. It is hard to see everyone else seem to be ignorant, even willingly ignorant, of these horrible dragons.

But how then does the world function, if effectively every program we have has monsters hiding in its exponential state space?

The answer is that generally the number of paths the program will take through the state space is polynomial. Those exponential spaces are available but they are far from equally available, they are not uniformly randomly chosen from. Hence, it is not terribly difficult to end up with programs that are nominally disasters where literally 99.99999999999999999999...% of the possible state space of the program is "wrong" yet they happily hum along for years at a time, because the 0.00...001% of the state space they ever get into is correct.

A simple sort of thing where this can happen is a threaded program that doesn't use concurrency primitives correctly, yet, requests come in slowly, perhaps even regularly, and tend to run to completion before the next one comes in. A theoretical disaster of a program can run for long periods of time quite correctly.

I've seen several code bases like this. I think of them as the code bases where every time something went wrong, the programmers basically went in and started hitting the code base with a stick. They'd fix the bug presenting itself, but they'd probably introduce 5 more, but each with a lesser probability. Then a couple of those come up, and they hit those with a stick, and introduce more bugs in principle, but fix the two from the original batch that came up. Maybe a couple of years later the third bug from that third batch finally comes up and they patch around it. I just spent the last 1.5 years rewriting such a code base. It's a disaster. It's a seething mass of bugs, both the ones they gave up trying to fix because they couldn't hit it hard enough, and the ones that are potentially there from all the stick-hitting that has been done. No structure. No coherence. Formal methods? Ha! It doesn't even have any testing in it and basically can't by its nature. But if you keep running around the loop, shove enough input through it, and keep hitting it with a stick, it will, eventually, basically work. Yea, though I walk through the Valley of Bugs, I will fear no errors, because all the evil has already befallen me.

The mismatch between formal advocates and us normies (which, though I am very sympathetic to formal methods, I've never actually gotten to use them for anything non-trivial myself, so I include myself in the latter set) is that formal advocates believe the rest of the world either does or should desire to remove all the dragons from the full exponential state space, whereas the rest of the world is really only concerned about the state spaces they will actually hit, which is exponentially less than the possible parts of the state space.

The reason you see someone like Amazon use formal methods to prove things for things like S3 is that they are hit so hard and in so many circumstances that they don't get to hide. In theory even in such a situation the full state space may not be covered, but the coverage is so intense and extreme that de facto the easiest thing to do is just pretend absolutely anything can happen, that any conceivable bug will be hit, and therefore it is worth it to go to a full formal methodology to prove that there are no dragons anywhere, or at the very least, fully characterize anything you couldn't dispose of. Kernels have a similar situation. But honestly, very little code is hit that hard, so it's not too surprising that people often don't seek formal methods out. Plus, the consequences need to be severe for anyone to care, e.g., office suites are probably nightmares in their full state space but if it crashes, well, generally, not much bad stuff happens to anyone.

I'd say a formal methods salesman needs a clear explanation as to how they can help with the polynomial common path. They can't expect to scare people with the dragons lying in exponential space because most people can't see them, even if you point at them, and that's when you sound like a kook rather than someone helpful. And there you run into the fact that, as the post explains in a completely different way, a lot of times the answer is that formal methods don't have as much to offer as it may seem like, because we non-formal programmers do have some tooling that is broadly, if not perfectly, adequate to the task of handling the polynomial-type state spaces, by testing them, constraining them, etc.

(In this post I have somewhat sloppily used the term "polynomial", so don't worry about it too much. It's a sort of amortized, limited sort of term, based on the real consequences of the state space on the code. For example, a text editor is plainly "exponential" in state space because the set of all possible text files is obviously exponential... but in practice, you don't generally have problems in a text editor where the editor crashes because the 1024'th character was an "a" instead of a "b". (Such things happen, but they are clearly exceptional, generally not hard fixes, and generally ultimately due to some other combination of bugs and not "really" that the character was "wrong".) So in pratice, despite the theoretically-exponential nature of text files, the complexity actually experienced by the programmer is nowhere near that full exponential space. What you end up with instead is generally a relatively small set of issues; excessively long lines, characters you didn't expect to see, handling emoji wrong, many issues, but text editor programmers don't experience specific 25-character long strings crashing the program, and find themselves dedicating months upon months to finding all the other such strings that specifically crash the program. The experience of the exponential state space is not exponential in practice and the 'real paths' through the program can be characterized through the elimination of information as something much simpler than the true exponential space. If it was, no non-trivial program would work, ever. Technically it's probably still exponential but compared to the theoretical exponentiality, so much vaster, it's still effectively polynomial by comparison.)

I'm working on a formal model now and I'm playing with spin and p-lang to see which is better. Not a fan of tla+

Well, have you tried only asking 4 times the money for 4 times the time? :)