[FOM] What is a proof?

[John McCarthy]

De Millo, Lipton and Perlis were mistaken in several matters.

1. They, and many of their opponents, confused performance
specifications of programs of programs operating in the world with
their input-output specifications.  The latter can be verified knowing 
the programming language and the properties of the functions involved
in the program.  To verify the performance specifications involves
facts about the world, some of which may even be social.

2. Formal program verification and hardware verification have been
used for many years, especially since the Intel floating point
division catastrophe.