Re:Formal Verification Creates Hacker-Proof Code
by obastani on Friday October 21, 2016 @04:36PM
(#12764485)
It's impossible to guarantee that your theorem prover is bug free -- for example, if it has a bug that causes it to always return "correct", then it proves its own correctness, even though it is clearly wrong.
This is not to say that self-hosting isn't useful, since most bugs are not likely to be of this form.
This is not to say that self-hosting isn't useful, since most bugs are not likely to be of this form.