CompCert

> 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

> Is the question "what is the first byte?" any more or less problematical for a {base, offset} pointer than it is for a multi-byte integer, where place value matters? Shifting and bit-masking integers are operations that make sense. Storing an int in memory and loading back only one of its bytes is equivalent to loading it all, then shifting and masking. It's meaningful, thus you do need to model the bits faithfully. In contrast, shifting and masking pointers is (with some exceptions) not meaningful. Neither is it meaningful to store one of these in memory and to load back only part of it. It makes sense to use a more abstract, symbolic model for bytes of such values. For whatever it's worth, the author's solution for bytes is the same as CompCert's: https://github.com/AbsInt/CompCert/blob/3939a1ccfdb86795e9fd...

It was more like they are from a strange haskell realm. Take a look at the ideal mathematical (verified) C compiler written in Coq. I find it neat: https://github.com/AbsInt/CompCert