Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-28T18:46:28.489Z Has data issue: false hasContentIssue false
  • English
  • Français

Social processes, program verification and all that

Published online by Cambridge University Press:  07 September 2009

ANDREA ASPERTI ,
HERMAN GEUVERS  and
RAJA NATARAJAN
ANDREA ASPERTI
Affiliation:
Dept. of Comp. Sci., Univ. of Bologna, Mura Anteo Zamboni 7, 40127 Bologna, Italy Email: [email protected]
HERMAN GEUVERS
Affiliation:
Dept. of Comp. Sci., Radboud Univ. Nijmegen and Tech. Univ. Eindhoven, The Netherlands Email: [email protected]
RAJA NATARAJAN
Affiliation:
School of Tech. and Comp. Sci., Tata Institute of Fundamental Research, Mumbai 400 005, India Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 5 , October 2009 , pp. 877 - 896
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Alkassar, E., Bogan, S. and Paul, W. J. (2009) Proving the correctness of client/server software. Sadhana 34 (1)145–191.CrossRefGoogle Scholar
Altenkirch, T., McBride, C. and McKinna, J. (2005) Why dependent types matter. (Available at http://sneezy.cs.nott.ac.uk/epigram/.)Google Scholar
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.Google Scholar
Asperti, A. and Ricciotti, W. (2009) About the formalization of some results by Chebyshev in number theory. In: Proc. of TYPES'08. Springer-Verlag Lecture Notes in Computer Science 5497 19–31.CrossRefGoogle Scholar
Avigad, J., Donnelly, K., Gray, D. and Raff, P. (2007) A formally verified proof of the prime number theorem. ACM Trans. Comput. Log. 9 (1).CrossRefGoogle Scholar
Barbanera, F. and Berardi, S. (1996) A symmetric lambda calculus for classical program extraction. Information and Computation 125 (2)103–117.CrossRefGoogle Scholar
Boolos, G. (1984) Don't eliminate cut. Journal of Philosophical Logic 13 373–378.CrossRefGoogle Scholar
Bos, J. V. D. (1979) Letter to the editor. Communications of the ACM 22 623.Google Scholar
Bourbaki, N. (1968) Theory of Sets, Elements of mathematics, Addison Wesley.Google Scholar
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T. and Smith, S. F. (1986) Implementing Mathematics with the Nuprl Development System, Prentice-Hall.Google Scholar
Coquand, T. (2008) Draft of the Formath Project.Google Scholar
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ölkel, M. (eds.) SemWiki. CEUR Workshop Proceedings 360.Google Scholar
Corbineau, P. and Kaliszyk, C. (2007) Cooperative repositories for formal proofs – 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–234.CrossRefGoogle Scholar
De Millo, R. A., Lipton, R. J. and Perlis, A. J. (1979) Social processes and proofs of theorems and programs. Commun. ACM 22 (5)271–280.CrossRefGoogle Scholar
Dewar, M. (2000) Special issue on OpenMath. ACM SIGSAM Bulletin 34.Google Scholar
Dijkstra, E. W. (1986) On a cultural gap. Mathematical Intelligencer 8 (1)48–52.CrossRefGoogle Scholar
Dold, A. and Vialard, V. (2001) A mechanically verified compiling specification for a lisp compiler. In: Proc. of FSTTCS 2001. Springer-Verlag Lecture Notes in Computer Science 2245 144–155.CrossRefGoogle Scholar
The Economist (2005) Proof and beauty. The Economist, 31st March 2005.Google Scholar
Fateman, R. (2001) A critique of OpenMath and thoughts on encoding mathematics. (Available at http://www.eecs.berkeley.edu/~fateman/papers/openmathcrit.pdf.)Google Scholar
Feit, W. and Thompson, J. G. (1963) Solvability of groups of odd order. Pacific Journal of Mathematics 13 775–1029.CrossRefGoogle Scholar
Fowler, M. (2000) The New Methodology. (Available at http://www.martinfowler.com/articles/newMethodology.html.)Google Scholar
Geuvers, H. (2009) Proof Assistants: history, ideas and future. Sadhana 34 (1)3–25.CrossRefGoogle Scholar
Girard, J.-Y., Lafont, Y. and Taylor, P. (1989) Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.Google Scholar
Gonthier, G. (2007) The four colour theorem: Engineering of a formal proof. In: Proc. of ASCM 2007. Springer-Verlag Lecture Notes in Computer Science 5081.Google Scholar
Gonthier, G. (2008) Formal proof – the four color theorem. Notices of the American Mathematical Society 55 1382–1394.Google Scholar
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E. and Thery, L. (2007) A modular formalisation of finite group theory. In: The 20th International Conference on Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 4732 86–101.CrossRefGoogle Scholar
Hales, T. C. (2005) A proof of the Kepler conjecture. Ann. Math. 162 1065–1185.CrossRefGoogle Scholar
Hales, T. C. (2007) The Jordan curve theorem, formally and informally. The American Mathematical Monthly 114 882–894.CrossRefGoogle Scholar
Hales, T. C. (2008) Formal proof. Notices of the American Mathematical Society 55 1370–1381.Google Scholar
Hall, C., Hammond, K., Jones, S. P. and Wadler, P. (1996) Type classes in Haskell. ACM Transactions on Programming Languages and Systems 18 241–256.CrossRefGoogle Scholar
Halmos, P. (1985) I want to be a Mathematician: An Automathography, Springer-Verlag.Google Scholar
Hamid, N. A., Shao, Z., Trifonov, V., Monnier, S. and Ni, Z. (2003) A syntactic approach to foundational proof-carrying code. J. Autom. Reasoning 31 (3-4)191–229.CrossRefGoogle Scholar
Hardy, G. H. (1928) Mathematical proof. Mind 38 1–25.Google Scholar
Harrison, J. (2007) Floating-point verification. J. UCS 13 (5)629–638.Google Scholar
Harrison, J. (2008) Formal proof – theory and practice. Notices of the American Mathematical Society 55 1395–1406.Google Scholar
Hoare, C. A. R. (1969) An axiomatic basis for computer programming. Commun. ACM 12 (10)576–580.CrossRefGoogle Scholar
Howard, W. A. (1980) The formulae-as-types notion of construction. In: Seldin, J. P. and Hindley, J. R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press 479–490.Google Scholar
Hutcheon, P. D. (1995) Popper and Kuhn on the evolution of science. Brock Review 4 (1/2)28–37.Google Scholar
Klein, G. (2005) Verified Java bytecode verification. Information Technology 47 (2)107–110.Google Scholar
Klein, G. (2009) Operating system verification – an overview. Sadhana 34 (1)27–69.CrossRefGoogle Scholar
Lakatos, I. (1976) Proofs and Refutations: The Logic of Mathematical Discovery, Cambridge University Press.CrossRefGoogle Scholar
Lamport, L. (1979) Letter to the editor. Communications of the ACM 22 624.Google Scholar
Langley, S. P. (1891) Experiments in Aerodynamics, Kessinger Publishing.Google Scholar
Lecat, M. (1939) Erreurs de mathématiciens: des origines à nos jours, Ancienne Librairie Castaigne, Brussels.Google Scholar
Lee, J. K. (2002) Philosophical perspectives on proof in mathematics education. Philosophy of Mathematics Education Journal 16.Google Scholar
Leinenbach, D., Paul, W. J. and Petrova, E. (2005) Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), IEEE Computer Society 2–12.CrossRefGoogle Scholar
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–54.CrossRefGoogle Scholar
MacKenzie, D. (2005) What in the name of Euclid is going on here? Science 207 (5714)1402–1403.Google Scholar
Maurer, W. D. (1979) Letter to the editor. Communications of the ACM 22 625–629.Google Scholar
Necula, G. C. and Lee, P. (1996) Proof-carrying code. Technical Report CMU-CS-96-165, Carnegie Mellon University.Google Scholar
Parigot, M. (1992) Lambda-mu calculus: An algorithmic interpretation of classical natural deduction. In: Proc. of the Logic Programming and Automated Reasoning International Conference LPAR'92. Springer-Verlag Lecture Notes in Computer Science 624 190–201.CrossRefGoogle Scholar
Popper, K. (1948) Logic without assumptions. Aristotelian society proceedings 47 251–292.CrossRefGoogle Scholar
Popper, K. (1963) Conjectures and Refutations. The Growth of Scientific Knowledge, Routledge.Google Scholar
Prawitz, D. (1965) Natural Deduction: a proof theoretical study, Almqvist and Wiksell.Google Scholar
Schieber, P. (1987) The wit and wisdom of Grace Hopper. OCLC Newsletter 167.Google Scholar
Sozeau, M. and Oury, N. (2008) First-class type classes. In: TPHOLs 278–293.CrossRefGoogle Scholar
Strecker, M. (1998) Construction and Deduction in Type Theories, Ph.D. thesis, Universität Ulm.Google Scholar
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–27.CrossRefGoogle Scholar
Wadler, P. and Blott, S. (1989) How to make ad-hoc polymorphism less ad hoc. In: POPL '89: Proc. of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM 60–76.CrossRefGoogle Scholar
Wenzel, M. (1997) Type classes and overloading in higher-order logic. In: TPHOLs 307–322.CrossRefGoogle Scholar
Wenzel, M. (1999) Isar – a generic interpretative approach to readable formal proof documents. In: Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 1690 167–184.CrossRefGoogle Scholar
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.)Google Scholar
Wiedijk, F. (2007) The Qed manifesto revisited. In: Matuszwski, R. and Zalewska, A. (eds.) From Insight to Proof, Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, University of Białystok 10 (23) 121–133.Google Scholar