[eudox]

The breadth and depth to which SQLite is tested[0] is both admirable and inspiring.

It's not just "internal" tests, like unit tests or things that can be run from client C programs, but tests of all kinds of hard-to-simulate external situations like out-of-memory and power failure situations.

[0]: https://www.sqlite.org/testing.html

[nickpsecurity]

That is simply amazing write-up. I'd still not call it a high-assurance system given some things missing. Yet, the amount of rigor in the testing phase could easily be the baseline for that niche in that it exceeds about anything I've seen. There's basically so little I could suggest on code or testing side that I'm not going to even bother here given how marginal it would be due to effort already put in. Just too well-done for mere speculations.

I also noted that the assert section essentially does Design-by-Contract. This is a subset of formal specification that's prime value is in preventing interface errors (vast majority in big apps) and supporting formal verification. Done in design/spec phase in high-assurance since both Edsger Dijkstra and Margaret Hamilton independently discovered technique's value. Done at language-level since Eiffel due to Bertrand Meyer. Good to see that, even if not all techniques, they're doing the 80/20 rule to get most benefit out of what formal specs they're using. Also allow you to easily enable run-time checks if you can accept performance hit. Nice.