Hacker News Reader

Comment by pests | Hacker News Reader

Everyone always praises SQLite

> As of version 3.42.0 (2023-05-16), the SQLite library consists of approximately 155.8 KSLOC of C code [...] the project has 590 times as much test code and test scripts - 92053.1 KSLOC.

https://www.sqlite.org/testing.html

View on HN

I once found a confirmed bug in SQLite one time, and it’s the highlight of all my OSS bug reports.

Interestingly enough I found it while fuzz testing a query builder and cross testing it against PostgreSQL, MySQL and an in-memory filtering engine I wrote.

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 popular now) are for.

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.

Link to how SQLite is tested, for anyone who's curious: 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://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.

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.

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.

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.

That's the same link I posted in the original comment, JSYK.

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.

You can do many things other than testing:

- use a memory safe language

- formal verification (multiple implementations even)

- build a simulator like FoundationDB did

Reply on news.ycombinator.com