News for hackers. Stuff that matters.
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.

There are no comments on this comment yet.