To a large extent, yes, a system can check itself. E.g., Bob Boyer tells me that one of the successes of proof-checking has been to prove that the garbage-collector of the system underlying one proof-checker was correct (collected all and only garbage). More and more HW is being proven correct -- e.g., after the Pentium floating point debacle in the 1990's, AMD worked with Boyer's group to prove that their float unit worked correctly. At 08:47 AM 3/3/2006, Eugene Salamin wrote:
Such a computer program would be as intricate as the proofs it is expected to verify, and is subject to the same human error. There cannot be certainty of correctness of a proof without certainty of the correctness of the proof-checking software. Could the program check itself?
Gene