> 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 quick

> 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). [1] https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert