Abstract
In this paper I will discuss the fundamental ideas behind proof assistants: What are they and what is a proof anyway? I give a short history of the main ideas, emphasizing the way they ensure the correctness of the mathematics formalized. I will also briefly discuss the places where proof assistants are used and how we envision their extended use in the future. While being an introduction into the world of proof assistants and the main issues behind them, this paper is also a position paper that pushes the further use of proof assistants. We believe that these systems will become the future of mathematics, where definitions, statements, computations and proofs are all available in a computerized form. An important application is and will be in computer supported modelling and verification of systems. But there is still a long road ahead and I will indicate what we believe is needed for the further proliferation of proof assistants.
Keywords. Proof assistant; verification; logic; software correctness; formalized
mathematics.
| Original language | English |
|---|---|
| Pages (from-to) | 3-25 |
| Journal | Sadhana : Academy Proceedings in Engineering Sciences (Indian Academy of Sciences) |
| Volume | 34 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 2009 |
Fingerprint
Dive into the research topics of 'Proof assistants : history, ideas and future'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver