Re:Formal Verification Creates Hacker-Proof Code
by Houshalter on Friday October 21, 2016 @11:38PM
(#12767019)
You don't need to prove that Peano arithmetic is consistent! You just need to prove that the theorem prover doesn't contain any bugs, i.e. that it correctly implements peano arithmetic. That's a much lower bar, and theorem provers have verified themselves in the past.
[ Parent
| on HN ]
There are no comments on this comment yet.