--- Edwin Clark <eclark@math.usf.edu> wrote:
On Fri, 3 Mar 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?
The proof checker would be a program and not a proof, so the proof checker would not be designed to check the correctness of the program.
Then the project will require a program checker in addition to a proof checker.
It seems that the best one could do is to construct a proof that the proof checker works and ask the proof checker to check that.
And also, we will ask the program checker to check itself in addition to checking the proof checker.
Of course, like any human enterprise there is the possibility of error. Can we perform any task with a guarantee that there will be no error?
If we could, then there would be no need for automated proof checking or automated program checking.
As long ago as the 1970s I recall hearing of a specialty in computer science called automatic proof verification. Googling around I find many references. For example there is Edmund Clarke at Carnegie Mellon who describes his research interest as: Automatic verification of computer hardware and software: http://www.cs.cmu.edu/~emc/15-398/
Also Wikipedia mentions a system at http://en.wikipedia.org/wiki/Hoare_logic called Hoare logic which was designed "to reason about the correctness of computer programs with the rigour of mathematical logic".
--WEC
There appears to be a basic problem with automated program checking. You have to provide two inputs, the program to be checked, and a description of what the program is supposed to do. But this description will have to be constructed by error-prone humans, and so we still have the problem of verifying the correctness of the descripton. Indeed if the description language is less confusing and less prone to mistakes than the program language, the description language should supplant the program language. What better way is there to create a program, than to describe what you want, and let the computer do it for you. Gene __________________________________________________ Do You Yahoo!? Tired of spam? Yahoo! Mail has the best spam protection around http://mail.yahoo.com