> "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.

This "quote" is probably bogus. When I was at lunch with Knuth once (brag, brag), someone asked him where he said that. Knuth said he couldn't recall saying it and he doubted that he ever said it, because he would not attempt to prove code without also testing it. Then he said it might be a paraphrase (not a quote) from an analysis he made of an assembly language program where he did not have hardware with that instruction set available to him.