Comment by andai

15 days ago

SQLite: 92 million lines of tests

Dijkstra: Tests can only prove the presence of bugs, never their absence!

38 comments

andai

Reply
otterley  15 days ago

Everyone knows that tests don't prevent all bugs. But they are very good at preventing known bugs from recurring in the future.

  • layer8  14 days ago

    Everyone doesn’t seem to know that, because tests are often cited as a way to ensure that AI-generated code is correct.

    • andai  14 days ago

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

      2 replies →

ameliaquining  15 days ago

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

0x457  15 days ago

It can prove absence of specific bugs though.

  • inigyou  14 days ago

    no it can't. what if this bug is still there but the timing window is now one CPU instruction?

    • aw1621107  14 days 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.

      8 replies →

    • kccqzy  14 days ago

      Then it’s a different bug: they fixed a bug with a wider timing window and introduced a new bug with a narrower timing window.

fghorow  15 days ago

Testing:

The union of a lot of necessary conditions is not a sufficient condition. But it might be good enough for software.

namelosw  14 days ago

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