[FOM] What is a proof?

Alasdair Urquhart 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
 	to fail.

I recommend the article highly.

Alasdair Urquhart

More information about the FOM mailing list