5 ms·
SQLite: 92 million lines of tests Dijkstra: Tests can only prove the presence of bugs, never their absence!
by andai 3mo ago
SQLite: 92 million lines of tests
Dijkstra: Tests can only prove the presence of bugs, never their absence!
- otterley 3mo agoEveryone knows that tests don't prevent all bugs. But they are very good at preventing known bugs from recurring in the future.
- layer8 3mo agoEveryone doesn’t seem to know that, because tests are often cited as a way to ensure that AI-generated code is correct.
- andai 3mo agoI was very excited about formal proofs, which are now very cheap to produce, in service of validating AI generated code. But I had a funny experience recently where an agent implemented an entire feature completely wrong (exactly backwards, actually, in a way that defeated the purpose, introduced security issues etc.). It happily supplied tests for the new functionality, and all the tests passed. What I realized was, even formal verification wouldn't have helped here -- it would have just written a mathematical proof that the incorrect functionality was correctly implemented! So there's a gap here, where first, the human's intention needs to be formally specified (by the human, or at least the human needs to be able and willing to verify it), and then the slopswarm can hack away at it...
- otterley 3mo ago> first, the human's intention needs to be formally specified This never changed with AI; in fact, I think it made this need more visible than it ever had been before. You can't get away with not being able to describe in detail what you want. As with working with humans, any ambiguities will be interpreted, and not always in the way you hoped.
- layer8 3mo ago> the human's intention needs to be formally specified Yes, that has always been the case with formal proofs. Even a mathematical proof with Lean is useless if the proven formal statement doesn’t match what the mathematician meant. And that’s why humans working with formal languages won’t be going away. Natural language is imprecise by nature, even when we have precise ideas in mind. In that case, it’s often better to specify what we mean in a formal language than in natural language.
- 0x457 3mo agoIt can prove absence of specific bugs though.
- inigyou 3mo agono it can't. what if this bug is still there but the timing window is now one CPU instruction?
- aw1621107 3mo ago> what if this bug is still there but the timing window is now one CPU instruction? I think a model checker or something similar that can exhaustively cover a search space would suffice, though at that point I think the boundary between "test" and "formal verification" becomes somewhat fuzzy.
- inigyou 3mo agoSo, a proof, not a test.
- dist-epoch 3mo agoDonald Knuth: Beware of bugs in the above code; I have only proved it correct, not tried it.
- krupan 3mo agoThe perfect yang to Dijkstra's yin
- ameliaquining 3mo agoI admit to curiosity as to whether static analysis could have caught this. E.g., Rust's type system (yeah yeah I know) catches all data races, unless they originate in unsafe code, which this one might or might not have; a hypothetical Rust SQLite would probably need a lot of unsafe (https://github.com/tursodatabase/turso https://github.com/tursodatabase/turso has 556 unsafe blocks in the core), and I don't have a sense of whether the particular part that contained this bug would be included in that.
- jhhh 3mo agoThere was a post recently using TLA to model this issue and (re)discover the bug: https://news.ycombinator.com/item?id=48730953 https://news.ycombinator.com/item?id=48730953.
- ameliaquining 3mo agoInteresting. I don't think this kind of technique could realistically have caught the bug in advance, though; you're not going to model the entire codebase in TLA+, so the investigation in that post modeled just the parts that turned out in hindsight to be relevant.
- fragmede 3mo ago> you're not going to model the entire codebase in TLA+ Not by hand in the olden days but with AI to help with it, why not?
- j16sdiz 3mo agoBecause AI have a recall of 80% or 90% at best. While it might be better than some human, it won't hit the 100% TLA+ modeling aims
- ameliaquining 3mo agoLLMs are not at the point where they can reliably complete this kind of task without making mistakes. The model checker can tell you whether the formal design specification contradicts itself, but it can't tell you whether it matches the implementation, nor whether it matches the programmers' intentions. And it's too much for humans to review by hand. This is importantly different from formal code verification, in which the specification that needs to match the programmers' intentions is small enough to review, while the bulk of the LLM's output is proof tactics and such, which don't need human review because the verifier guarantees* that they're right. I suppose you could just tell Fable "hey try using TLA+ to look for bugs in this code" and see whether it finds any. * Uh, usually. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
- _justme 3mo agohttps://news.ycombinator.com/item?id=18442941 https://news.ycombinator.com/item?id=18442941
- andai 3mo agoJesus Christ. I have this comment saved, but it gets me every time.
- fghorow 3mo agoTesting: The union of a lot of necessary conditions is not a sufficient condition. But it might be good enough for software.
- namelosw 3mo agoThe idea of testing is to sample and test the paths you care about, mostly business workflows, not to enumerate infinite combinations. It's an art to come up with a great test suite that covers just enough and minimizes overlap, not only survives but also helps with refactoring.
- altilunium 3mo agoprobatio diabolica https://en.wikipedia.org/wiki/Probatio_diabolica https://en.wikipedia.org/wiki/Probatio_diabolica https://07th-expansion.fandom.com/wiki/Devil%27s_Proof https://07th-expansion.fandom.com/wiki/Devil%27s_Proof
- heresie-dabord 2mo agoObligatory UNIX fortune: "Computer Science can be thought of as the post-Turing decline in formal methods."