Mathematical Structures in Computer Science

Paper

Social processes, program verification and all that

ANDREA ASPERTIa1, HERMAN GEUVERSa2 and RAJA NATARAJANa3

a1 Dept. of Comp. Sci., Univ. of Bologna, Mura Anteo Zamboni 7, 40127 Bologna, Italy Email: asperti@cs.unibo.it

a2 Dept. of Comp. Sci., Radboud Univ. Nijmegen and Tech. Univ. Eindhoven, The Netherlands Email: herman@cs.ru.nl

a3 School of Tech. and Comp. Sci., Tata Institute of Fundamental Research, Mumbai 400 005, India Email: raja@tifr.res.in

Abstract

In a controversial paper (De Millo et al. 1979) at the end of the 1970's, R. A. De Millo, R. J. Lipton and A. J. Perlis argued against formal verifications of programs, mostly motivating their position by an analogy with proofs in mathematics, and, in particular, with the impracticality of a strictly formalist approach to this discipline. The recent, impressive achievements in the field of interactive theorem proving provide an interesting ground for a critical revisiting of their theses. We believe that the social nature of proof and program development is uncontroversial and ineluctable, but formal verification is not antithetical to it. Formal verification should strive not only to cope with, but to ease and enhance the collaborative, organic nature of this process, eventually helping us to master the growing complexity of scientific knowledge.

(Received April 25 2009)

(Revised May 03 2009)

(Online publication September 07 2009)