You Don’t Know Jack About Formal Verification

5 points by eatonphil

The post unfortunately has the same kind of non-arguments that have been repeated forever, and lacks key understanding of the other side.

People generally don't "skip" formal verification because the cost is prohibitive -- companies actually pay through their nose for all different kinds of software -- they do it because alternative techniques like testing are more widely understood, allow for easier hiring, and provide gains more incrementally. This was true pre-LLMs and is still true today. https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods

And I say this as someone who likes formal methods! It's not enough for your thing to be cheaper. You have to compare it with the alternatives. Lots of non-functional requirements are often important but formal verification has little to say about those. Being able to test UIs and database calls is valuable. Actual applications care about things working end to end, not just the "core logic" (whatever that means).

k749gtnc9l3w

I think it's even yet worse.

How much of the interop code needs to handle the data known not to satisfy any coherent enough structural rules? How much of the business logic is about negotiating an interpretation of an inherently contradictory specification coming from outside? Of course one wants to rely on tests, I already know this doesn't satisfy any specification with reasonable provenance!

There is a spectrum from «doing a thing correctly» to «being compatible with random garbage frmo the other side», and much of the problems we see are from too many things being on the compatibility side and also full of churn.

ETA: my perspective is of someone who has both co-authored a paper about guessing protocol invariants from small instances then asking an automated theorem prover to prove correctness in general, and has had to use in practice a data source that theoretically has documented checksumming rules but does not follow them. I… see some distance between what I need/want/plausibly hope for in those two cases.