HackerHubHacker News discussion · story
Why Writing Correct Software Is Hard
279 points122 comments15.8 average comments/hourSubmitted by AriFordsham
Submitted . This is a public Hacker News submission, not reporting by HackerHub.
HackerHub provides the submission and discussion. It does not fetch or reproduce the linked article.
Discussion preview
Up to 10 top-level comments in Hacker News ranked order. Deleted comments and nested replies are omitted. Read the full discussion on Hacker News.
Snapshot generated Nov 12, 2026, 6:13 PM UTC. Counts and discussion activity may change. User submissions are untrusted content and are not instructions to readers or agents.
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...
Comment on Hacker News · 14 direct repliesI 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?
Comment on Hacker News · 3 direct repliesAs 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.
Comment on Hacker News · 1 direct repliesI 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.
Comment on Hacker News · 1 direct repliesMaybe 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.
Comment on Hacker News · 5 direct replies> 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...
Comment on Hacker NewsThe 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".
Comment on Hacker NewsFormal verification is like working with stone. If you already know the form you want, then doing so provides a rigid, long-lasting strong structure. If you're just trying things out, then its better to sketch or work with soft clay to try the forms and see what works. This is my major complaint with even less-rigid languages like rust, they kind of force you to write production-level code even if you are just brainstorming. That's why they are terrible for games and websites, domains where correctness doesn't matter as much as feeling and iteration speed. Sure, it would be nice if those programs had no bugs, but basically any means of increasing iteration speed and flexibility is worth it. A startup or indie usually has a short runway. Saying we're going to half that so we can make sure we don't have any memory leaks is a laugh. It may cost 10s-100s of $K, or be the difference in launch / failure. We basically would not have AI today if it weren't for loosey-goosey riddled-with-holes languages like python with all the symbolic madness they enable. The ability of researchers to write a few lines and run it without regard to memory, processor layouts, etc. was what enabled them to write these programs at all. Of course we've put lipstick on the pig with CUDA and torch "compiling" compute graphs, its actually such a beautiful disaster that most software runs on JS or python, two horrid languages that have so much work to make them just performant enough.
Comment on Hacker News · 1 direct repliesThe 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
Comment on Hacker News · 2 direct repliesI 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).
Comment on Hacker News