4 ms·
> In SQLite, the presence of assert(X) means that the developers have a proof that X is always true. Almost impossible to prove anything in a sufficiently comp
by kalecserk 7y ago
> In SQLite, the presence of assert(X) means that the developers have a proof that X is always true.
Almost impossible to prove anything in a sufficiently complex system such as SQLite. The difference between assert and always seems arbitrary IMHO
- saagarjha 7y agoThe difference is that assert has been “proved” to be true, while ALWAYS is merely thought to be true.
- chris_wot 7y agoI’m still uncertain what they mean by “prove” though.
- kevingadd 7y agosqlite has extremely thorough test coverage with something approaching 100% branch coverage and such wide production usage it's basically proven that a lot of this stuff works.
- nn3 7y agoMost (all?) of the production usage probably doesn't enable the assert though.
- hcs 7y agoProbably the same mechanism by which most proofs work, not fully formal but it seems to follow. Without the proofs in comments (or transitively through other asserts) it's up to the reader to recreate the argument, though. The purpose is to be more explicit than a comment, I suspect, using the same notation as the code.
- viraptor 7y agoYou're only using it locally for specific invariants. That doesn't have to depend on the system's complexity. For example assert(2+2==4) works the same, regardless of it's only a one line app, or in the middle of an OS kernel.