#### 15 Dec 2002 moshez»(Master)

raph: thanks. The link you gave does give an explanation, but an incorrect one, I'm adraid :) Think about what you know: going from the design (even a fairly specific one) to a fully working program is, at the very least, a factor of 20 in length. Let's treble it for non-trivial proofs like Jordan, in which many techniques which are hard to formalize as stand-alone lemmas are assumed as trivial, and we have a factor of 60. So, basically, if we assume the "classical" Jordan proof is on the order of a 200k, then we estimate the formal proof to be 60*200k = 3MB. That's 3MB of no-comments, "assembly" level math. Now, sure, the checker will find bugs in that proof. How long do you think it would take to completely debug that insane amount of mathematical proof? Uniquifying names, proving each non-trivial set operation usage, and so on.

Yes, it is embarassing to have a referee find an error in your paper. I doubt it happens very often: mathematicians, before submitting papers, go over them with a comb looking for errors. Then they ask colleagues to look at them. Then they give talks about them. This is a much more efficient use of the time then translating it to assembly so the proof checker can verify it.

The author of the link you gave seems to argue that the proof checker will be able to fill in the missing details, because "computers are good at boring details". This is about equivalent to a statement that computers will be good at auto-debugging, because they're good at boring details. Computers are good at repetitive details, not mere boring ones. Significant AI increase has to happen before computers can fill in the missing details, even those which would be easy for first-year students.

Now, on the question of correctness proof, my skepticallity has no strict basis in experience, so I cannot argue as strongly. However, I do tend to think that in non-trivial programs, specifying the correctness correctly will be almost as non-trivial as writing the program.