3 ms·
100% code coverage explores an absolutely miniscule portion of the state space of any given program. This is why formal methods are a thing.
by Quekid5 6y ago
100% code coverage explores an absolutely miniscule portion of the state space of any given program. This is why formal methods are a thing.
- dathinab 6y agoYes especially for something fairly complex like an sql engine with views and full text search. Through then it also seems that many of the newer bugs sl seem to be around more advanced features which sometimes can be disabled on compiler time. (newer=after they integrated fuzzing into their tested) I wonder if it makes sense for Oses to ship two versions of sqlite one for the small local "trusted" database case and one for the sqlite as file format case which had many features disabled, only allowing the core subset of sqlite. Through if you provide some "evergreen" software you can anyway just include your own version of sqlite. Potentially statically linked in.
- juskrey 6y agoFormal methods have formal assumptions.
- Quekid5 6y agoYes? A huge portion of what a database does is amenable to formal methods. You can even come up with a reasonable rudimentary formal model of a physical machine/CPU and check against that. Sure, the model of the machine may be wrong in subtle ways, but when you discover that, you fix it and recheck your model of a database against the updated model of a physical machine. That said... don't use a language with trivially allows for out-of-bounds indexing, etc. (SQLite was started when there were really few other good options, so that's understandable.)