[FOM] What is a proof?

[Alasdair Urquhart]

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