4 ms·
I think what many commenters are missing is why this is important. Invariants like this allow one to prove the correctness of their code. That may not seem lik
by mabbo 8y ago
I think what many commenters are missing is why this is important.
Invariants like this allow one to prove the correctness of their code. That may not seem like a big deal most of the time, but imagine you're working on a satellite that's going to Jupiter, where a bug in the code could mean 10 years from now a billion dollar project gets scuttled. Imagine you're building subroutines that will go into 10,000 pacemakers next year. Imagine you're writing the navigation logic for a cruise missile.
There are many times where proving your code correct is taken very, very seriously. Invariants are a tool to do so more easily.
- deleted 8y ago[deleted]
- ramtatatam 8y agoTo prove the correctness of your code you would write tests in similar way as SQLite does, no? They have, like, 100x more lines of code for tests than actual code they test?
- jacobajit 8y agoTest cases do not establish proof. There could always be another rare edge case.
- heartofgold 8y agoWhat jacobajit said. Or here's what Dijkstra said: "Program testing can be used to show the presence of bugs, but never to show their absence!" Dijkstra (1970)
- mabbo 8y agoUnit tests demonstrate correctness. That's another useful tool in the tool box. But proofs are more than just that. Imagine trying to unit test all possible cases of Pythagorean theorem being correct vs a single proof in a few lines of descriptive logic.