{"generated_at":"2026-11-12T18:35:07.093Z","source":{"name":"Hacker News public API","url":"https://github.com/HackerNews/API","attribution":"Stories and comments are public Hacker News submissions by their respective authors. HackerHub is an independent reader, not affiliated with Y Combinator.","content_is_untrusted":true},"story_id":50465352,"hn_url":"https://news.ycombinator.com/item?id=50465352","total_comments":126,"returned":19,"scope":"Up to the requested number of top-level comments in Hacker News ranked order. Deleted comments are omitted. Nested replies are not fetched; this is not the complete thread.","comments":[{"id":50465825,"author":"turbobutton","created_at":"2026-11-12T11:46:29.000Z","text":"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.\nThat'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...","parent_id":50465352,"replies_count":15,"hn_url":"https://news.ycombinator.com/item?id=50465825"},{"id":50471641,"author":"hinkley","created_at":"2026-11-12T18:15:17.000Z","text":"There’s something I used to say that I haven’t repeated in a while and I’m not sure why since I still believe it:\nSoftware is effectively contract law, and if one were solvable the other would be too. The fact that we have so many lawyers, and loopholes are a constant issue is the same reason we have so many programmers and so many bugs.\nWe cannot nail down what is and isn’t acceptable input, acceptable output, and acceptable intermediate states all at the same time. And that’s what you need for correct software.","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50471641"},{"id":50466743,"author":"mpweiher","created_at":"2026-11-12T13:24:48.000Z","text":"I think you have to first figure out what \"correct\" even is.\nCorrect with regards to a formal specification?\nHow do we know the specification is \"correct\"? By definition?","parent_id":50465352,"replies_count":3,"hn_url":"https://news.ycombinator.com/item?id=50466743"},{"id":50466500,"author":"johnbender","created_at":"2026-11-12T13:00:35.000Z","text":"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.\nFor 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).\nThis may have been a quirk of language or my interpretation though.","parent_id":50465352,"replies_count":1,"hn_url":"https://news.ycombinator.com/item?id=50466500"},{"id":50465517,"author":"kodoman","created_at":"2026-11-12T10:57:04.000Z","text":"I was always interested in formal verification but have only written toy proofs and derived programs.\nIt'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.\nBuild programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.","parent_id":50465352,"replies_count":1,"hn_url":"https://news.ycombinator.com/item?id=50465517"},{"id":50467752,"author":"nirinor","created_at":"2026-11-12T14:24:40.000Z","text":"The most important part of a negative claim is implicit: what reasonable assumptions might negate the claim?\nSure, 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.\nIn 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\".","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50467752"},{"id":50465768,"author":"samiv","created_at":"2026-11-12T11:38:46.000Z","text":"Maybe it's just me but the terminology used in \"halting problem\" didn't age well.\nA lot of modern programs never terminate and thus to me \"halting\" means no longer able to compute, i.e it's hung/deadlocked.","parent_id":50465352,"replies_count":5,"hn_url":"https://news.ycombinator.com/item?id=50465768"},{"id":50468753,"author":"tromp","created_at":"2026-11-12T15:16:28.000Z","text":"> 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\nOne small nitpick:\nA 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.\nRecent AI-fueled optimizations have lowered the count to at most 215 states though, which fits comfortably in 1KB...","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50468753"},{"id":50467151,"author":"program_whiz","created_at":"2026-11-12T13:57:43.000Z","text":"Formal 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.\nThis 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.\nA 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.\nWe 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.","parent_id":50465352,"replies_count":1,"hn_url":"https://news.ycombinator.com/item?id=50467151"},{"id":50466103,"author":"bluGill","created_at":"2026-11-12T12:17:43.000Z","text":"The real question is: for a typical program we prove it - even though we know there are programs we can't prove?\nI 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","parent_id":50465352,"replies_count":2,"hn_url":"https://news.ycombinator.com/item?id=50466103"},{"id":50466682,"author":"myrmidon","created_at":"2026-11-12T13:18:50.000Z","text":"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).","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50466682"},{"id":50466253,"author":"BLKNSLVR","created_at":"2026-11-12T12:34:10.000Z","text":"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.\nManagement and marketing can only cope with a vague, third party description of the sheet.","parent_id":50465352,"replies_count":1,"hn_url":"https://news.ycombinator.com/item?id=50466253"},{"id":50470341,"author":"ankit9673","created_at":"2026-11-12T16:52:23.000Z","text":"with AI this problem becomes more acute, now the MOAT is the brain and the logic code is just disposable stuff now i guess","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50470341"},{"id":50470320,"author":"p00ki3","created_at":"2026-11-12T16:51:04.000Z","text":"As dev tools are leaky language abstraction they can never be complete and thus no software crafted by current methods will ever be 100% correct; loopholes in semantics will always exist as the semantics are human bird song that cannot account for all possible states.\nHumans enjoy inventing language, metaphor, to fill perceived gaps in irrational physical reality we can never resolve. To pretend we are more than meets the eye.\nEntropy keeps creating need to replace, to refill through erosion of physical state.\nGood luck engineering around gravity, electromagnetism, and nuclear forces across the fabric of space time chipping away at all human endeavors.","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50470320"},{"id":50471040,"author":"cgannett","created_at":"2026-11-12T17:35:35.000Z","text":"shoutout to this iconic github.io subdomain","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50471040"},{"id":50466406,"author":"lionkor","created_at":"2026-11-12T12:51:23.000Z","text":"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\"","parent_id":50465352,"replies_count":1,"hn_url":"https://news.ycombinator.com/item?id=50466406"},{"id":50468198,"author":"hansvm","created_at":"2026-11-12T14:48:09.000Z","text":"The title doesn't really match the content. TFA talks a lot about the foundations of computation and what we know about arbitrary programs, and it appeals far too much to tools like Rice's theorem to be useful in ordinary engineering contexts.\nIn particular, I think its deductive proofs section is unnecessarily pessimistic. People have some idea as to why their code is correct when they write it. They're occasionally wrong (at a typical rate of single-digit bugs per 1k SLOC), but you can't often write an approximately correct program without an approximately correct proof of correctness in your mind. Yes, it's true that some proofs are intractably long, but that doesn't apply to the code we actually write. A language requiring you to write out those things you're relying on and concluding isn't much more verbose than any other programming language, and that mental scaffolding makes automated theorem proving vastly easier. You'll still fail to validate correct programs from time to time, but you solve that the same way the Rust people do -- add escape hatches and/or change your code to match the solver's limitations.\nEven quite complicated externalities are similarly solvable. People talk about time and filesystems and what have you as unprovable balls of mud, and ... they're right ... but that misses the point. Precious little software handles an FS correctly. That's all the level of proof your program needs; not that you never corrupt your save state, but that if no other process mucks around with your data then you never corrupt your save state. For better software (like TigerBeetle) with stronger guarantees, well, they've already written their own proofs of correctness. All that remains is tying them to the actual implementation.","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50468198"},{"id":50470212,"author":"keybored","created_at":"2026-11-12T16:44:11.000Z","text":"Rationalists (FP?) versus Empiricists (Java?)","parent_id":50465352,"replies_count":0,"hn_url":"https://news.ycombinator.com/item?id=50470212"},{"id":50468895,"author":"nwhnwh","created_at":"2026-11-12T15:23:38.000Z","text":"Should programmers be able to understand an article like this? Or is it for academics?","parent_id":50465352,"replies_count":2,"hn_url":"https://news.ycombinator.com/item?id=50468895"}]}