Comment by nickpsecurity

10 years ago

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.