29 Jul
2003
29 Jul
'03
12:20 a.m.
John McCarthy wrote: << When a long computer calculation is an important part of the proof of a mathematical theorem, we should ask for proof (preferably both computer-checked and hand checked) that the program does the advertised calculation. For example, we want a proof that if the calculation comes out, the four color conjecture is true.
This is of course desirable, but brings up a new question: where does this stop? A typical "verification of correctness" of a sizeable computer program involves the application of another program. Then we need to know that the verification program is valid and was used properly. Etc. --Dan