Don wrote:
I agree with Walter's statement that ALL of the components are unreliable, and I think it's important to realize that proofs are the same. Even in the case where the program perfectly implements the algorithm, there can be bugs in the proof.
Also, the hardware running the correct program can fail.
