3 ms·

What the fuck. If they're investing that much then why don't they just go straight to formal verification. This is what things like frama-c (or whatever's popul

• gavinhoward 3y ago
  The problem is that effort to do formal verification goes exponential beyond a certain point. seL4 is around 10-12 KLoC, and it took a decade of effort from multiple people to make it happen. At the size of SQLite, especially where they have to operate on platforms with different behavior (as an OS, seL4 is the platform), formal verification is just too much effort. All that said, your reaction is totally understandable.
  • tonyarkles 3y ago
    Link to how SQLite is tested, for anyone who's curious: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html There's also an interesting thing where formal verification requires a formal specification, which afaik there isn't one for SQLite. One of the toughest problems that someone would run into trying to put together a formal specification for code as widely deployed as SQLite boils down to Hyrum's Law[1]: on a long enough time scale, all observable behaviours of your system become interfaces that someone, somewhere depends on. That massive suite of test cases isn't a formal specification but given that it achieves 100% branch coverage that implies to me that it: - pretty tightly bounds the interface without formally specifying it - also pretty tightly constrains the implementation to match the current implementation Which, when you have as many users as you do with SQLite, is probably a fair way of providing guarantees to your users that upgrading from 3.44.0 to 3.45.1 isn't going to break anything you're using unless you were relying on explicitly-identified buggy behaviour (you'd be able to see the delta in the test cases if you looked at the Fossil diffs). [1] https://www.hyrumslaw.com https://www.hyrumslaw.com
    • er4hn 3y ago
      https://corecursive.com/066-sqlite-with-richard-hipp/ https://corecursive.com/066-sqlite-with-richard-hipp/ is an interesting interview with the lead developer for SQLite about the inspiration and work that went into that testing as well.
    • SAI_Peregrinus 3y ago
      Also a formal specification can have bugs. Formal verification checks that the code matches the spec, not that the spec implements all desired behaviors and no undesired behaviors.
      • IshKebab 3y ago
        You're right, though it's worth noting that you can also use formal verification to verify properties about the specification! For example you can verify that a security system doesn't allow privilege escalation.
        • SAI_Peregrinus 3y ago
          Yep, though of course it's still on you to remember to verify everything you care about. Actually writing out all your requirements in a formal (or just programming) language is the hard part of programming.
    • pests 3y ago
      That's the same link I posted in the original comment, JSYK.
• summerlight 3y ago
  Because formal verification doesn't scale at the moment. There are a relatively few number of experts on formal method around the globe and some of them need to work on SQLite indefinitely unless you're okay with just one-off verification. Frama-C has a different background because it's from Inria, the institution with many formal method experts.
• datadeft 3y ago
  You can do many things other than testing: - use a memory safe language - formal verification (multiple implementations even) - build a simulator like FoundationDB did