Abstract
Computer-aided proof is attracting an ever-wider audience. Hitherto over-represented in the field of computer science, where it was born, it has begun to arouse a certain enthusiasm among mathematicians. However, the two communities do not share the same cultural backgrounds.
This paper presents an assertive computer scientist's point of view on the foundations of a proof assistant and the very relevance of this question. Our thesis is based on the proof-program equivalence, which will be used both as a theoretical paradigm and as a sociological approach. Our vision is both pluralistic and monistic. Monistic, because the choice of a foundation has many practical consequences on the use of a proof assistant, so we need to design the best system. Pluralist, because we don't believe in a single mathematical language : each sub-field expresses itself in extremely different languages. This disparity is well known to computer scientists, who use numerous programming languages on the same computer. This tension is resolved through compilation. We'll take a look at a few techniques inspired by this field, and look ahead to a bright future with a plethora of high-level proof systems.
