Why Correct Software Is Hard: The Mathematical Limits of Verification
Why Writing Correct Software Is Hard
Drawing on computability and complexity theory, this essay argues that writing correct programs is fundamentally hard, not merely a matter of better tools. The halting theorem and its corollaries—Rice's theorem, the Busy Beaver function—show that verifying arbitrary program properties is undecidable, and that the difficulty grows faster than any computable function. Even small programs, like a 1919-state Turing machine, can have behavior independent of ZFC set theory, meaning their termination cannot be proven.
The cost of correctness – like the energy cost of reducing entropy – is a result of the “natural laws” of computation, that cannot possibly be avoided.
- turbobutton
I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world. Any software that's processing inputs and provides complex workflows to humans has to necessarily deal with the endless vagaries of reality.
That's not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth...
- mpweiher
I think you have to first figure out what "correct" even is.
Correct with regards to a formal specification?
How do we know the specification is "correct"? By definition?
- johnbender
As best I can tell the article wrongly conflates Rices Theorem with the idea that one can’t prove something about the small program generated by Yedidiya and Aaronson but that’s not what Rices Theorem tells us. Instead it tells us that we can’t come up with a general method to determine yes or no correctly for all programs whether a program reaches a given point.
For a given program and a one off proof one can prove many things or if we over approximate by assuming loops terminate we can prove many things soundly with the risk of rejecting programs that are sometimes correct (eg type systems).
This may have been a quirk of language or my interpretation though.
- kodoman
I was always interested in formal verification but have only written toy proofs and derived programs.
It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.
Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.
- tromp
> a Turing machine with 1919 control states which cannot be proven to terminate (i.e., it is “independent of ZFC”). This machine is so small that it comfortably fits in a 4K challenge
One small nitpick:
A 4K challenge normally refers to code that fits in 4KB, but a straightforward encoding of a 1919 state TM takes 19192(2+11) = 49894 bits, or 6237 bytes, over 6KB.
Recent AI-fueled optimizations have lowered the count to at most 215 states though, which fits comfortably in 1KB...
- nirinor
The most important part of a negative claim is implicit: what reasonable assumptions might negate the claim?
Sure, by Rice's theorem, no program can decide whether an arbitrary function always computes the sum of its two inputs. But that's only because we are allowing arbitrarily difficult-to-analyze implementations of the sum function. So this theorem co-exists with the fact that simple implementations of sum can be proven correct.
In this light I think the best conclusion is "to write correct software in reasonable time, we must use easy to analyze languages and program styles".
- bluGill
The real question is: for a typical program we prove it - even though we know there are programs we can't prove?
I don't care about the examples given, I care about my word processor, web browser and such. Can we prove them - putting limits on the scripting language
- myrmidon
I found it interesting how the lower bound for the BB(6) champion (2-symbol 6-state busy beaver) dates the article: It gives >10^36534, but the current champion (mxdys 2025) is >10↑↑10↑↑10↑↑8 (10↑↑8 is a power tower 10^10^10^10... eight high, and the expression is resolved right to left, so 10↑↑10↑↑8 is already completely unimaginably large).