Social Processes and Proofs of Theorems and Programs

It is argued that formal verifications of
programs, no matter how obtained, will not play the
same key role in the development of computer science and software
engineering as proofs do in mathematics.  Furthermore the absence
of continuity, the inevitability of change, and the complexity of
specification of significantly many real programs make the form
al verification process difficult to justify and manage.  It is felt
that ease of formal verification should not dominate program
language design.

CACM May, 1979

De Millo, R.
Lipton, R.
Perlis, A.

Formal mathematics, mathematical proofs,
program verification, program specification

2.10 4.6 5.24

CA790501 DH June 5, 1979  2:23 PM

3140	5	3140
3140	5	3140
3140	5	3140
3178	5	3140
3076	6	3140
3140	6	3140
3142	6	3140
3179	6	3140
3180	6	3140
3181	6	3140
3182	6	3140