I usually love Graydon's posts, but this one -- like many articles about formal methods -- may be misleading for most readers unfamiliar with the field. It's a

I usually love Graydon's posts, but this one -- like many articles about formal methods -- may be misleading for most readers unfamiliar with the field. It's a little like reporting an order of magnitude improvement in transmuting lead into gold without mentioning that there are 29 further orders of magnitude to go before the method is cost-effective in practice. Does no aliasing make formal verification significantly easier? Absolutely! Does it mean we can expect a practical and cost-effective way to verify real world programs? Not even remotely. Yes, some programs, circuits, and program components are formally verified every day, but they are the exception rather than the rule; they are relatively very small and they are constructed in particular careful ways. Nice properties that allow local reasoning about some other properties are important but do not materially affect the way we can assure the correctness of mainstream software with sound methods. A reasonable, real-world program that would take a million years of effort to verify without such properties will only take 100,000 years of effort to verify with them. That is good and it is even useful in practice because a program that would take a year to verify could now take a month -- making it actually cost-effective -- only the number of such programs to begin with is vanishingly small in the grand scheme of things. A program in a language with no heap, no pointers, no integers -- only boolean variables -- and no loops larger than two iterations (the language is nowhere near Turing complete) cannot be practically verified (by reduction from TQBF). Not in theory, not in practice, and there aren't even heuristic methods that cover many real world instances of such programs (of course, some such programs could happen to be easily verifiable). It can be made to work for some properties (like memory safety) -- we say that we can make these invariants inductive or composable -- but it turns out that that's not nearly good enough for what software needs. Back in the seventies and eighties, and even nineties, the hope was that while the "worst case" complexity of verifying programs was known to be intractable, perhaps certain local guarantees and structures employed by programming languages could move us away from the worst case. It has since been proven to not be the case. Even the hope that programs people actually write are far enough from the worst case for good heuristic methods to emerge, and even that now seems to not be the case. Many years ago I gave a talk covering the relevant findings: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity The main result is that the verification most interesting properties that we'd like to verify does not compose. I.e. if we can prove a property for components P1...Pn, then proving that property for P1 ○ ... ○ Pn (where ○ is some composition such as a subroutine call or message passing) does not just grow super-polynomially in n (which would be good!), but super-polynomially in the size of each of the components, i.e. it would be just as hard to prove if everything was not decomposed. I.e. correctness does not decompose. Yes, some important programs can be soundly verified and various local properties can make that easier, which is useful but because of software is growing much faster than the scale of effective formal verification and because we've learned more results about the complexity of software verification, end-to-end verification of "ordinary" software appears further away today than it did 50 years ago. That is why there's a shift in research of software assurance toward unsound methods. A focus on soundness does not, I believe, help the cause of more correct software, but distracts away from more techniques that have proven more fruitful. This gap between "we can verify quite a bit" and "what we can verify is a drop in the ocean" -- both of which are true at the same time -- is something that is often missing from discussions of formal methods.