Re:Formal Verification Creates Hacker-Proof Code
by nickpsecurity on Friday October 21, 2016 @01:20PM
(#12762438)
That and the Godel one above. For first point, they could link to a presentation on high-assurance systems showing one needs a combination of specs, proofs, testing, and human review for max assurance. For the second, the alternative is showing how the prover problem is greatly reduced by using simple, proof checkers and/or logics in the process that are easy to verify by hand.
"Beware of people slinging around the famous Knuth quote as if it invalidated progress in program proving." - Me
(Not a reference to you personally, but I think that this quote is too often used to disparage all work on program provers, rather than as just—as I take it to be—pointing out that, no matter how good your prover is, you should still check your code.)