Comment by JadeNB
10 years ago
> "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth
"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.)
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.