In the analogy between programming and theorem-proving, programs correspond to proofs. When mathematicians informally check a proof, they are usually judging wh

In the analogy between programming and theorem-proving, programs correspond to proofs. When mathematicians informally check a proof, they are usually judging whether a complete proof could be produced, not whether the presented proof is a complete correct proof. Programmers are not given the same affordance.