FOM: RE: Computer-verified theorems...III

[Matt Insall]

Andrej:
<Snip>
A typical mathematician who has not had much experience with
programming might think that 1)--4) are not an issue. He will say that
we must just make sure that the program has been written correctly,
and that the hardware must be designed correctly. BUT WE HAVE NO IDEA
HOW TO DO THAT IN PRACTICE!


Matt:
I am aware that the problem of doing this is combinatorially explosive.
However, if a particular program is important enough to a particular deep
enough pocket, is it not possible to at least accomplish what I described
previously for 1) in practice?  Moreover, is it not the case that problems
2), 3) and 4) can be solved, as long as someone throws enough money at them?
What is needed is a careful and exhaustive dissection of the problems, I
would think.

Matt Insall