Résumé
Depuis quelques années, la preuve assistée par ordinateur séduit un public de plus en plus large. Jusque-là surreprésentée dans le domaine de l'informatique où elle était née, elle a commencé à susciter chez les mathématiciens un engouement qui a fait bruire ses fuseaux dans des sphères prestigieuses. Néanmoins, cet appel d'air ne s'est pas fait sans incompréhension, les deux communautés ne partageant pas nécessairement les mêmes arrière-fonds culturels.
Le but de cet exposé est de présenter un point de vue informaticien assumé sur la question des fondements d'un assistant à la preuve et de la pertinence même de cette dernière. En effet, une certaine méfiance règne chez les mathématiciens vis-à-vis de la logique, et ce plus particulièrement en France. La thèse que nous développerons s'appuie sur l'équivalence preuve-programme, qui sera utilisée aussi bien comme paradigme théorique que comme approche sociologique. Notre vision est à la fois pluraliste et moniste. Moniste, car le choix d'une fondation a de nombreuses conséquences pratiques dans l'utilisation quotidienne d'un assistant à la preuve. Il convient donc de s'attacher à concevoir un système qui a le plus de propriétés désirables possible. Pluraliste, car nous ne croyons pas en un langage unique des mathématiques : chaque sous-domaine tend à s'exprimer dans des langages de surface extrêmement différents, sans même parler de la diversité des techniques de preuve. Cette disparité est heureusement bien connue des informaticiens, qui utilisent de nombreux langages de programmation au quotidien sur le même ordinateur. Cette tension est résolue au moyen de la compilation, qui réduit la variété des langages de haut niveau à un unique langage bas-niveau et tatillon, l'assembleur. Nous exposerons quelques techniques inspirées de ce domaine qui pourraient constituer les premières marches vers la sortie de l'enfer du bas-niveau que constitue aujourd'hui la preuve assistée par ordinateur, et évoquerons un avenir radieux dans lequel cohabitent pléthore de systèmes de preuve de haut-niveau.
