{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T08:40:42Z","timestamp":1769330442754,"version":"3.49.0"},"reference-count":63,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2009,9,7]],"date-time":"2009-09-07T00:00:00Z","timestamp":1252281600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2009,10]]},"abstract":"<jats:p>In a controversial paper (De Millo <jats:italic>et al<\/jats:italic>. 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.<\/jats:p>","DOI":"10.1017\/s0960129509990041","type":"journal-article","created":{"date-parts":[[2009,9,7]],"date-time":"2009-09-07T08:29:08Z","timestamp":1252312148000},"page":"877-896","source":"Crossref","is-referenced-by-count":19,"title":["Social processes, program verification and all that"],"prefix":"10.1017","volume":"19","author":[{"given":"ANDREA","family":"ASPERTI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"HERMAN","family":"GEUVERS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"RAJA","family":"NATARAJAN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,9,7]]},"reference":[{"key":"S0960129509990041_ref45","article-title":"Philosophical perspectives on proof in mathematics education","volume":"16","author":"Lee","year":"2002","journal-title":"Philosophy of Mathematics Education Journal"},{"key":"S0960129509990041_ref43","volume-title":"Experiments in Aerodynamics","author":"Langley","year":"1891"},{"key":"S0960129509990041_ref41","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139171472"},{"key":"S0960129509990041_ref38","first-page":"28","article-title":"Popper and Kuhn on the evolution of science","volume":"4","author":"Hutcheon","year":"1995","journal-title":"Brock Review"},{"key":"S0960129509990041_ref48","first-page":"1402","article-title":"What in the name of Euclid is going on here?","volume":"207","author":"MacKenzie","year":"2005","journal-title":"Science"},{"key":"S0960129509990041_ref33","first-page":"1","article-title":"Mathematical proof","volume":"38","author":"Hardy","year":"1928","journal-title":"Mind"},{"key":"S0960129509990041_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"S0960129509990041_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02444-3_2"},{"key":"S0960129509990041_ref46","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.51"},{"key":"S0960129509990041_ref37","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0960129509990041_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S0960129509990041_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1084-9"},{"key":"S0960129509990041_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_8"},{"key":"S0960129509990041_ref23","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129509990041_ref8","first-page":"623","article-title":"Letter to the editor","volume":"22","author":"Bos","year":"1979","journal-title":"Communications of the ACM"},{"key":"S0960129509990041_ref63","first-page":"121","volume-title":"Studies in Logic, Grammar and Rhetoric","author":"Wiedijk","year":"2007"},{"key":"S0960129509990041_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BF00247711"},{"key":"S0960129509990041_ref39","first-page":"107","article-title":"Verified Java bytecode verification","volume":"47","author":"Klein","year":"2005","journal-title":"Information Technology"},{"key":"S0960129509990041_ref27","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2005.162.1065"},{"key":"S0960129509990041_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0001-5"},{"key":"S0960129509990041_ref54","volume-title":"Natural Deduction: a proof theoretical study","author":"Prawitz","year":"1965"},{"key":"S0960129509990041_ref35","first-page":"1395","article-title":"Formal proof \u2013 theory and practice","volume":"55","author":"Harrison","year":"2008","journal-title":"Notices of the American Mathematical Society"},{"key":"S0960129509990041_ref18","unstructured":"The Economist (2005) Proof and beauty. The Economist, 31st March 2005."},{"key":"S0960129509990041_ref29","first-page":"1370","article-title":"Formal proof","volume":"55","author":"Hales","year":"2008","journal-title":"Notices of the American Mathematical Society"},{"key":"S0960129509990041_ref32","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021012.97318.e9"},{"key":"S0960129509990041_ref9","volume-title":"Theory of Sets","author":"Bourbaki","year":"1968"},{"key":"S0960129509990041_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"S0960129509990041_ref2","unstructured":"Altenkirch T. , McBride C. and McKinna J. (2005) Why dependent types matter. (Available at http:\/\/sneezy.cs.nott.ac.uk\/epigram\/.)"},{"key":"S0960129509990041_ref20","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1963.13.775"},{"key":"S0960129509990041_ref58","unstructured":"Tristan J.-B. and Leroy X. (2008) Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Proc. of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008 17\u201327."},{"key":"S0960129509990041_ref25","first-page":"1382","article-title":"Formal proof \u2013 the four color theorem","volume":"55","author":"Gonthier","year":"2008","journal-title":"Notices of the American Mathematical Society"},{"key":"S0960129509990041_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_12"},{"key":"S0960129509990041_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_13"},{"key":"S0960129509990041_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297660"},{"key":"S0960129509990041_ref44","volume-title":"Erreurs de math\u00e9maticiens: des origines \u00e0 nos jours","author":"Lecat","year":"1939"},{"key":"S0960129509990041_ref13","doi-asserted-by":"crossref","unstructured":"Corbineau P. and Kaliszyk C. (2007) Cooperative repositories for formal proofs \u2013 a wiki-based solution. In: Kauers M. , Kerber M. , Miner R. and Windsteiger W. (eds.) Towards Mechanized Mathematical Assistants. Springer-Verlag Lecture Notes in Computer Science 4573 221\u2013234.","DOI":"10.1007\/978-3-540-73086-6_19"},{"key":"S0960129509990041_ref15","article-title":"Special issue on OpenMath","volume":"34","author":"Dewar","year":"2000","journal-title":"ACM SIGSAM Bulletin"},{"key":"S0960129509990041_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"S0960129509990041_ref24","article-title":"The four colour theorem: Engineering of a formal proof. In: Proc. of ASCM 2007","volume":"5081","author":"Gonthier","year":"2007","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129509990041_ref3","unstructured":"Asperti A. , Padovani L. , Sacerdoti Coen C. and Schena I. (2000) Content-centric logical environments. Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science."},{"key":"S0960129509990041_ref60","doi-asserted-by":"crossref","unstructured":"Wenzel M. (1997) Type classes and overloading in higher-order logic. In: TPHOLs 307\u2013322.","DOI":"10.1007\/BFb0028402"},{"key":"S0960129509990041_ref11","unstructured":"Coquand T. (2008) Draft of the Formath Project."},{"key":"S0960129509990041_ref19","unstructured":"Fateman R. (2001) A critique of OpenMath and thoughts on encoding mathematics. (Available at http:\/\/www.eecs.berkeley.edu\/~fateman\/papers\/openmathcrit.pdf.)"},{"key":"S0960129509990041_ref12","unstructured":"Corbineau P. , Geuvers H. , Kaliszyk C. , McKinna J. and Wiedijk F. (2008) A real semantic web for mathematics deserves a real semantics. In: Lange C. , Schaffert S. , Skaf-Molli H. and V\u00f6lkel M. (eds.) SemWiki. CEUR Workshop Proceedings 360."},{"key":"S0960129509990041_ref42","first-page":"624","article-title":"Letter to the editor","volume":"22","author":"Lamport","year":"1979","journal-title":"Communications of the ACM"},{"key":"S0960129509990041_ref10","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"Constable","year":"1986"},{"key":"S0960129509990041_ref28","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.2007.11920481"},{"key":"S0960129509990041_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0004-2"},{"key":"S0960129509990041_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF03023921"},{"key":"S0960129509990041_ref47","doi-asserted-by":"crossref","unstructured":"Leroy X. (2006) Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proc. of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA 42\u201354.","DOI":"10.1145\/1111037.1111042"},{"key":"S0960129509990041_ref49","first-page":"625","article-title":"Letter to the editor","volume":"22","author":"Maurer","year":"1979","journal-title":"Communications of the ACM"},{"key":"S0960129509990041_ref50","unstructured":"Necula G. C. and Lee P. (1996) Proof-carrying code. Technical Report CMU-CS-96-165, Carnegie Mellon University."},{"key":"S0960129509990041_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0960129509990041_ref52","doi-asserted-by":"publisher","DOI":"10.1093\/aristotelian\/47.1.251"},{"key":"S0960129509990041_ref53","volume-title":"Conjectures and Refutations. The Growth of Scientific Knowledge","author":"Popper","year":"1963"},{"key":"S0960129509990041_ref55","article-title":"The wit and wisdom of Grace Hopper","volume":"167","author":"Schieber","year":"1987","journal-title":"OCLC Newsletter"},{"key":"S0960129509990041_ref56","doi-asserted-by":"crossref","unstructured":"Sozeau M. and Oury N. (2008) First-class type classes. In: TPHOLs 278\u2013293.","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S0960129509990041_ref62","unstructured":"Wiedijk F. (2001) Estimating the cost of a standard library for a mathematical proof checker. (Available at http:\/\/www.cs.ru.nl\/~freek\/notes\/mathstdlib2.pdf.)"},{"key":"S0960129509990041_ref57","unstructured":"Strecker M. (1998) Construction and Deduction in Type Theories, Ph.D. thesis, Universit\u00e4t Ulm."},{"key":"S0960129509990041_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"S0960129509990041_ref6","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0025"},{"key":"S0960129509990041_ref21","unstructured":"Fowler M. (2000) The New Methodology. (Available at http:\/\/www.martinfowler.com\/articles\/newMethodology.html.)"},{"key":"S0960129509990041_ref34","first-page":"629","article-title":"Floating-point verification","volume":"13","author":"Harrison","year":"2007","journal-title":"J. UCS"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129509990041","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T10:53:34Z","timestamp":1556621614000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129509990041\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,7]]},"references-count":63,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["S0960129509990041"],"URL":"https:\/\/doi.org\/10.1017\/s0960129509990041","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9,7]]}}}