HN

Comments (93)

• Menu

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

  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?
• 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 challengeOne 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...
• Menu

  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.
• 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.
• 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".
• Menu

  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
• program_whiz
  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.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.
• 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).
• Menu

  samiv
  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.
• Menu

  BLKNSLVR
  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.
• hansvm
  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.In 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.Even 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.
• Menu

  lionkor
  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"
• nwhnwh
  Should programmers be able to understand an article like this? Or is it for academics?
• 4lx87
  Instead of trying to prove undefined semantics conform to a spec, we could code using semantics that are correct by construction.There’s no need to “verify” a language that only permits correct programs. In other words, we can program with finite state machines and automata instead of Turing machines.
• stackedinserter
  Ok, my 1/100 of Goldbach IQ brain disagrees. Real life computer programs rarely operate in infinite precision numbers. We write business logic, API's and calculate salaries.How often we use full int16 for counting things? Even stuff like video frames we can easily limit size_t to fixed values like `{1920x1080, 1920x1080x3 , 1920x1080x1.5, 1080}` (representing common memory sizes for 420/RGB frames).So instead of validating the whole infinite space of all possible states, we can carve tiny tunnels in this hypercube and significantly reduce that surface of proof.
• Menu

  jdw64
  Sometimes I wonder whether Silicon Valley programmers take this kind of difficult programming as a given. I tend to think in terms of simple programs, and while formal verification isn't bad, I question whether that's really software development.I know that in the AI era, with code being generated in enormous quantities, formal verification is important. It is effective to some degree, but in my view, software that requires provable correctness is only a subset of all software, and I agree with the author that a kind of empiricism is the right approach. Because most of it is based on understanding a customer's "requirements." And if we consider that not all requirements can be formally proven mathematically, then in practice the line between where formal verification is used and where it isn't will become clearly drawn.Formal specification is the work of deciding where the target is, and formal verification is the work of hitting that target with an arrow. But most of software development is the work of deciding where the target ought to be. Formal specification is like shooting an arrow at a moving target and hitting the bullseye, but figuring out where to pin that target down is software development, and honestly, most of software development spends more time pinning the target's position. Especially in the AI era, even more so.
• arbor-group
  [flagged]
• suwapat
  [dead]
• wasabiz
  [dead]
• m3tazahmed
  [flagged]
• hn_submit
  TLDR: programming isn't math and therefore most programs cannot be proven correct.