This probably needs a rename, "SQLite: View Ticket" is not a terribly descriptive title.
That said, it's a little surprising to see a bug of this type in SQLite which generally has such solid test coverage... Oh well, nothing is bug free after all.
On the other hand this is the kind of bugs you'd expect to see when programmers rely too heavily on the tests to catch bugs.
It takes 20 lines to reproduce the bug minimally, and relies on a confluence of code-generator bugs. I believe most fuzzers would take a considerable amount of time to find a bug like this...
How are you suggesting a team on a very large project find this elsewise?
rely too heavily on the tests
Presumably they are to find it using something besides tests? Intuition? Casting lots? Code review?
I think the intention was to embrace formal methods, which "proves" the absence of bugs (to the limited extents though). For a heavily-used critical piece of code like SQLite the lack or weak use of formal methods might actually be a reasonable criticism.
EDIT: Not meant to say that the original comment was reasonable.
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.
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).