>This is what *assurance* is all about - recognising the value
>of having checked, even if the outcome is boringly satisfactory.
>The aircraft industry and many other industries put huge
>dollar values on assurance.
Airplanes crash. Proofs don't. Last year I asked if anyone could
give an example of a theorem which was published in a textbook
or reputable journal, accepted by the mathematicians who read
it and used by them in further work, and then found to be
false. No one ever came up with such an example.
It is an illusion to think that QED is needed to "verify" a proof,
such as the Wiles proof, that has received the intense scrutiny of
many competent mathematicians.
Programs, of course, do crash. QED could certainly be useful in
computer science and engineering, where the mathematics is
tedious, complex, and not at all intuitive. Victor Yodiaken made
this point very well in his message of July 5, 1993. If QED
provides assurance that computer systems (and other complex
systems) will perform according to their specifications, industry
will certainly put a huge dollar value on such assurance.
However, QED was originally conceived as a project comprising
"all of mathematics." If it is going to degenerate into a tool for
engineers, it is a waste of time (from a scientific standpoint).
What can QED offer pure mathematicians? This question may
have an answer, but the answer is not "verification."
Lyle