4 ms·
Automatic proof checkers still have bugs in them. However, one nice characteristic is that, since its algorithms are so general, i.e. about the language rather
by infinity0 6y ago
Automatic proof checkers still have bugs in them. However, one nice characteristic is that, since its algorithms are so general, i.e. about the language rather than about the problem you're solving (e.g. sorting), any bugs in the checker are either so common they hit every problem solution and are easily discovered and fixed, or so rare that it affects no real-world problem solutions.
- adrianN 6y agoThe kernel of an automatic proof checker is much easier to test and verify than the programs you verify using a proof checker though.
- chrisandchips 6y ago+1 verification tends to be the easy part.
- infinity0 6y agoSure, not all bugs are kernel bugs though.