Hacker News Reader

> 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

View on HN

You'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.

The difference is that assert has been “proved” to be true, while ALWAYS is merely thought to be true.

I’m still uncertain what they mean by “prove” though.

sqlite 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.

Most (all?) of the production usage probably doesn't enable the assert though.

Probably 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.

Reply on news.ycombinator.com