Re:Formal Verification Creates Hacker-Proof Code
by Senji on Friday October 21, 2016 @01:13PM
(#12762353)
In the general case, we could just ignore general recurrsion and circular definitions or self refferencing functions. Then we win.
[ Parent
| on HN ]
Re:Formal Verification Creates Hacker-Proof Code
by simondedalus on Friday October 21, 2016 @10:05PM
(#12766641)
The problem is that Gödel builds self-reference. It's not like Peano arithmetic has recursion or self-reference operators.
To put it another way, in order to disqualify self-reference, you would need to employ a higher order proof system--which gives the game away anyway.