- When a theorem in math is proven that is just the start of the process. If it is important enough it will be passed around the community and checked and rechecked. At some point if it survives scrutiny it will be accepted. (Makes you wonder about proofs in the literature that nobody reads- could they be false?)
- The people working in Program Verification want to give program-correctness the same confidence that we have in Math Theorems.
- This is not a good idea since Programs cannot be passed around the same way Math Theorem proofs can. (Makes you wonder about the Classification of Finite Simple Groups, or the Four Color Theorem which also cannot be passed around that easily.)
The comments on Program Verification do not really apply anymore since those people seem to have scaled down their claims to building tools to find bugs, and to automatic verification of Protocols written in a SPEC language, which seems far more plausible. (I'm not in the Program Verification Field so if someone wants to tell me I'm wrong, leave an intelligent comment.)
When I first read this article as a young grad students I was very impressed with what it said about math. YES, the proof is just the beginning, but constant checks and rechecks are needed.