Re:Formal Verification Creates Hacker-Proof Code
by abecedarius on Friday October 21, 2016 @07:39PM
(#12765880)
Technically, 3) No bugs in your proof checker. A bug-infested theorem prover can still be useful.
As long as I'm well-actuallying, 2) The proven properties establish my own informal goals. If a hacker's goals are also satisfied, well, maybe they want to DDoS the internet but it's Not My Problem.
As long as I'm well-actuallying, 2) The proven properties establish my own informal goals. If a hacker's goals are also satisfied, well, maybe they want to DDoS the internet but it's Not My Problem.