[FOM] What is a proof?
urquhart at cs.toronto.edu
Fri Jan 23 15:23:13 EST 2009
There is an article by the computer scientists
De Millo, Lipton and Perlis that I think
is very apposite to this thread. The authors
argue eloquently against ease of formal verification
being a criterion of language design. The article
is called "Social Processes and Proofs of Theorems
and Programs." It is easily available online --
just do a search for the title.
The authors sum up their main thesis as follows:
We believe that, in the end, it is
a social process that determines whether mathematicians
feel confident about a theorem--and we believe that,
because no comparable social process can take place
among program verifiers, program verification is bound
I recommend the article highly.
More information about the FOM