Résumé :

Étant donné l'adoption croissante des assistants à la démonstration, leurs noyaux – la partie critique du système – semblent une cible parfaite pour la vérification de programme : ils sont critiques, mais relativement simples et bien spécifiés. C'est un rêve ancien, mais malgré la maturité de la théorie des types et de la vérification de programme, on n'a toujours pas d'Agda, Rocq ou Lean vérifié. La difficulté centrale est que les noyaux reposent sur des invariants complexes, qui eux-même se basent sur des propriétés méta-théoriques fortes des systèmes de types/logiques sous-jacentes. Il est donc impossible de vérifier un noyau sans auparavant formaliser la méta-théorie de son système de types, une entreprise loin d'être évidente pour un langage réaliste.

Malgré ces difficulté, les choses changent rapidement, avec une multitude de projets explorant cet espace. Dans mon exposé, je donnerai un aperçu de ce paysage, présentant en particulier deux projets complémentaires auxquels j'ai récemment contribué : MetaRocq, qui vise à vérifier un noyau pour Rocq, en Rocq, et Logrel-Rocq, qui se concentre plutôt sur les aspects de méta-théorie formalisée.

----------
Given the growing use of proof assistants, their kernels are a natural target for program certification: they are critical, yet small and well-specified. This goal is not new, but despite the maturity of type theory and software verification, we are yet to see a certified Agda, Coq or Lean. The core difficulty is that kernels rely on complex invariants, which in turn rest on significant properties of the type system. In essence, we cannot certify a kernel without first formalising the meta-theory of its type system, a difficult endeavour for a realistic language.

However, things have been recently changing, with multiple new projects in this space. In my talk, I will give an overview of this landscape, and present two complementary formalisation projects in that direction: MetaRocq, which aims at verifying a kernel for Rocq, in Rocq, and Logrel-Rocq, which concentrates more on the formalised meta-theory aspects.