In a controversial paper at the end of 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 those 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, but to ease and enhance the collaborative, organic nature of this process, eventually helping to master the growing complexity of scientific knowledge.Curry-Howard analogy

Social processes, program verification and all that

ASPERTI, ANDREA;
2009

Abstract

In a controversial paper at the end of 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 those 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, but to ease and enhance the collaborative, organic nature of this process, eventually helping to master the growing complexity of scientific knowledge.Curry-Howard analogy
2009
A.Asperti; H.Geuvers; R.Natarajan
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/77500
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? 13
social impact