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