Abstract
For some years now, computer-aided proof has been attracting an ever-wider audience. Hitherto over-represented in the field of computer science, where it was born, it has begun to arouse a craze among mathematicians that has made its spindles rustle in prestigious spheres. Nevertheless, this appeal was not without misunderstanding, as the two communities do not necessarily share the same cultural backgrounds.
The aim of this paper is to present an assertive computer scientist's point of view on the question of the foundations of a proof assistant and the very relevance of the latter. Indeed, mathematicians, particularly in France, are wary of logic. The thesis we shall develop 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 in the day-to-day use of a proof assistant. It is therefore important to design a system that has as many desirable properties as possible. Pluralistic, because we don't believe in a single language of mathematics: each sub-field tends to express itself in extremely different surface languages, not to mention the diversity of proof techniques. Fortunately, this disparity is well known to computer scientists, who use numerous programming languages on a daily basis on the same computer. This tension is resolved by means of compilation, which reduces the variety of high-level languages to a single, fussy low-level language, assembler. We will present some techniques inspired by this field, which could be the first steps towards escaping the low-level hell that is computer-aided proof today, and evoke a bright future in which a plethora of high-level proof systems cohabit.
