Surprisingly SQLite does actually embrace formal methods in various places.
Such as, in their draft goals [0], under S30200, they outline a memory allocator goal by referring to a proof.
Though, if the parents goal was to imply that the whole of SQLite should be verified... I'm not convinced its entirely possible. Quite a lot of SQLite revolves around things around where the halting problem may come into play.
> Such as, in their draft goals [0], under S30200, they outline a memory allocator goal by referring to a proof.
By that argument every implementation of quicksort (say) would be using formal methods. But they aren't. There are some definitions of formal methods allowing this kind of "weaker" form, but for the sake of this discussion such methods do not prevent a particular class of bugs. Explicit goal statements are, while being a very good direction, informal.
> Though, if the parents goal was to imply that the whole of SQLite should be verified... I'm not convinced its entirely possible. Quite a lot of SQLite revolves around things around where the halting problem may come into play.
This is probably correct and I don't recommend to do so. Even CompCert [1], probably the single most verified C compiler, is not absolutely fully verified and of course there had been bugs in the unverified modules (codegen AFAIK). But formal methods can be partially applied to produce provably more correct code (in some metrics).
What things that SQLite does revolves around anything halting-problem related? Almost all SQLite queries are over a finite amount of data and have a well-specified legal solution set that barely requires recursion; WITH RECURSIVE doesn't have to halt but still has a well-defined semantics where it does. I think even most optimization problems on SQL queries are decidable; you have to want to do quite interesting things (like prove query subsumption) before you get into undecidability territory.
I see two main areas where the halting problem comes into play:
SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate.
SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate.
> SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate.
Under reasonable assumptions about I/O (POSIX APIs and stuff), you can certainly prove termination of such operations.
> SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate.
You don't have to always prove any VM program will terminate. You just have to show termination-preserving refinement of the SQLite code generator (as I alluded to in my other post). You don't even need types for this.
Almost all things you'd want to prove about a program are undecidable in the general case. That doesn't mean much about the particular case of your program.
A computer program should be written to never* deadlock, and that implies that the programmers have a vague proof sketch in their head of why it doesn't deadlock that could if needed be formalized as a proof.
*I'm sure there is some exception out there but it doesn't matter for this argument.
Such as, in their draft goals [0], under S30200, they outline a memory allocator goal by referring to a proof.
Though, if the parents goal was to imply that the whole of SQLite should be verified... I'm not convinced its entirely possible. Quite a lot of SQLite revolves around things around where the halting problem may come into play.
[0] http://www.sqlite.org/draft/sysreq.html