"Correctness Doesn’t Matter" Let me explain this in formal methods terms. As programs grow their state space naturally exponentially expands. One of the major

"Correctness Doesn’t Matter" 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.)