Why Writing Correct Software Is Hard

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...

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).

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.

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.

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

Only developers see software in it's full resolution. The rest of us see an abstraction; the sheet lying over the top of a device that will never actually be unveiled due to its grotesque appearance. The public can barely even handle the aesthetics of the sheet.

Management and marketing can only cope with a vague, third party description of the sheet.

Maybe it's just me but the terminology used in "halting problem" didn't age well.

A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.

[dead]

TLDR: programming isn't math and therefore most programs cannot be proven correct.

I adore that it has become normalized in vibe-coding circles to go "actually, maybe correctness doesn't exist! as long as it runs on my machine it's fine"