×

Social processes, program verification and all that. (English) Zbl 1178.68333

Summary: In a controversial paper at the end of the 1970s, R. A. De Millo, R. J. Lipton and A. J. Perlis [Math. Intell. 3, 31–40 (1980; Zbl 0455.68017)] 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Citations:

Zbl 0455.68017

Software:

Nuprl; Isar
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Hutcheon, Brock Review 4 pp 28– (1995)
[2] DOI: 10.1007/s12046-009-0002-4 · Zbl 1192.68432 · doi:10.1007/s12046-009-0002-4
[3] Howard, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism pp 479– (1980)
[4] Bos, Communications of the ACM 22 pp 623– (1979)
[5] DOI: 10.1007/BF00247711 · Zbl 0564.03005 · doi:10.1007/BF00247711
[6] DOI: 10.1145/363235.363259 · Zbl 0179.23105 · doi:10.1145/363235.363259
[7] DOI: 10.1006/inco.1996.0025 · Zbl 0853.68159 · doi:10.1006/inco.1996.0025
[8] Harrison, Notices of the American Mathematical Society 55 pp 1395– (2008)
[9] DOI: 10.1145/1297658.1297660 · Zbl 1367.68244 · doi:10.1145/1297658.1297660
[10] Harrison, J. UCS 13 pp 629– (2007)
[11] Asperti, Springer-Verlag Lecture Notes in Computer Science 5497 pp 19– (2009) · Zbl 1246.03026 · doi:10.1007/978-3-642-02444-3_2
[12] Hardy, Mind 38 pp 1– (1928)
[13] DOI: 10.1023/B:JARS.0000021012.97318.e9 · Zbl 1069.68038 · doi:10.1023/B:JARS.0000021012.97318.e9
[14] Wiedijk, Studies in Logic, Grammar and Rhetoric pp 121– (2007)
[15] Halmos, I want to be a Mathematician: An Automathography (1985) · doi:10.1007/978-1-4612-1084-9
[16] DOI: 10.1007/s12046-009-0004-2 · Zbl 1177.68045 · doi:10.1007/s12046-009-0004-2
[17] DOI: 10.1145/227699.227700 · Zbl 01936238 · doi:10.1145/227699.227700
[18] Wenzel, Springer-Verlag Lecture Notes in Computer Science 1690 pp 167– (1999) · doi:10.1007/3-540-48256-3_12
[19] Hales, Notices of the American Mathematical Society 55 pp 1370– (2008)
[20] Hales, The American Mathematical Monthly 114 pp 882– (2007)
[21] DOI: 10.1145/75277.75283 · doi:10.1145/75277.75283
[22] DOI: 10.4007/annals.2005.162.1065 · Zbl 1096.52010 · doi:10.4007/annals.2005.162.1065
[23] Gonthier, Springer-Verlag Lecture Notes in Computer Science 4732 pp 86– (2007) · Zbl 1144.68356 · doi:10.1007/978-3-540-74591-4_8
[24] Gonthier, Notices of the American Mathematical Society 55 pp 1382– (2008)
[25] Gonthier, Springer-Verlag Lecture Notes in Computer Science 5081 (2007)
[26] Schieber, OCLC Newsletter 167 (1987)
[27] Girard, Proofs and Types (1989)
[28] Prawitz, Natural Deduction: a proof theoretical study (1965) · Zbl 0173.00205
[29] DOI: 10.1007/s12046-009-0001-5 · Zbl 1192.68629 · doi:10.1007/s12046-009-0001-5
[30] Popper, Conjectures and Refutations. The Growth of Scientific Knowledge (1963)
[31] Popper, Aristotelian society proceedings 47 pp 251– (1948) · doi:10.1093/aristotelian/47.1.251
[32] Feit, Pacific Journal of Mathematics 13 pp 775– (1963) · Zbl 0124.26402 · doi:10.2140/pjm.1963.13.775
[33] Parigot, Springer-Verlag Lecture Notes in Computer Science 624 pp 190– (1992) · doi:10.1007/BFb0013061
[34] Maurer, Communications of the ACM 22 pp 625– (1979)
[35] Dold, Springer-Verlag Lecture Notes in Computer Science 2245 pp 144– (2001) · doi:10.1007/3-540-45294-X_13
[36] MacKenzie, Science 207 pp 1402– (2005)
[37] DOI: 10.1007/BF03023921 · Zbl 0586.68025 · doi:10.1007/BF03023921
[38] DOI: 10.1145/362001.362008 · Zbl 1049.68500 · doi:10.1145/362001.362008
[39] Klein, Information Technology 47 pp 107– (2005)
[40] DOI: 10.1109/SEFM.2005.51 · doi:10.1109/SEFM.2005.51
[41] DOI: 10.1145/359104.359106 · doi:10.1145/359104.359106
[42] Lee, Philosophy of Mathematics Education Journal 16 (2002)
[43] Lecat, Erreurs de mathématiciens: des origines à nos jours (1939) · JFM 61.0001.02
[44] Langley, Experiments in Aerodynamics (1891) · JFM 23.0984.04
[45] Constable, Implementing Mathematics with the Nuprl Development System (1986)
[46] DOI: 10.1145/359156.359160 · Zbl 0412.68014 · doi:10.1145/359156.359160
[47] Lakatos, Proofs and Refutations: The Logic of Mathematical Discovery (1976) · Zbl 0334.00022 · doi:10.1017/CBO9781139171472
[48] Bourbaki, Theory of Sets (1968)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.