Le mariage des effets et des assistants à la preuve – ProverFX

La correction formelle des logiciels gagne de plus en plus de terrain, avec une application paroxystique aux logiciels en médecine pouvant mettre en jeu la vie des patients, et les logiciels embarqués dans des véhicules autonomes, pour lesquels la sécurité des passagers est critique. Les démonstrateurs interactifs de théorèmes basés sur la théorie des types ont montré leur efficacité pour prouver la correction de logiciels importants comme la chaîne d'outils du projet DeepSpec. Cependant, ils souffrent d'une limitation majeure : l'absence d'effets. Cela signifie que, du point de vue de la programmation, tous les programmes certifiés sont purs, c'est-à-dire sans exception ni état mutable, ce qui entraîne des problèmes d'efficacité du code extrait. Cela signifie également, d'un point de vue logique, que nous n'avons accès ni au raisonnement classique ni à l'axiome du choix, ce qui entraîne des problèmes d'expressivité de la logique. En mettant de côté l'efficacité et l'expressivité, l'ajout d'effets permettrait d'aller au-delà du paradigme "tous les programmes et toutes les preuves doivent être entièrement spécifiés et terminés", qui empêche les développeurs de faire des prototypes et des tests rapides avant d'entrer dans le processus de certification en soi. Mais la raison de cette limitation est assez forte et connue depuis les années 90 : l'ajout naïf d'effets donne lieu à des assistants de preuve logiquement incohérents.

Récemment, mon groupe a ouvert une brèche par laquelle des effets peuvent être intégrés dans les assistants de preuve en apprivoisant la puissance des types dépendants grâce à une généralisation des univers de Grothendieck. Sur la base de cette approche radicalement nouvelle, le projet ProverFX fournira une famille d'assistants de preuve où des effets informatiques et logiques peuvent être ajoutés à la théorie initiale en utilisant des phases de compilation, sans corrompre la logique. Ces phases de compilation seront elles-mêmes certifiées à l'intérieur d'un assistant de preuve—ce qui, avec la certification du système original, permet de passer d'une base de code fiable à un paradigme de base théorique fiable. Ces extensions augmenteront considérablement le type de systèmes logiciels qui peuvent être certifiés par des ingénieurs non experts, ainsi que le type de preuves que les mathématiciens pourront formaliser.