Résumé
Le dernier cours de l’année a pris la forme d’une introspection. Tout au long du cours, nous avons utilisé un assistant à la démonstration (Coq) comme langage et comme outil de vérification. Comment formaliser et mécaniser la correction sémantique d’un tel outil ? Se pose immédiatement la question de la cohérence de la logique implémentée par l’outil. Une logique est cohérente si elle ne peut pas dériver de paradoxes ou autres énoncés absurdes.
Pour une logique fondée sur la théorie des types, comme celle de Coq, la cohérence correspond, au sens de Curry-Howard, à l’existence d’un type qui n’est pas habité (aucun terme clos n’appartient à ce type). Nous avons donné les grandes lignes d’une démonstration de cohérence dans le style de Curry-Howard, qui étend la démonstration de sûreté vue au cours précédent avec un nouvel impératif : la propriété de normalisation, « tout terme bien typé termine ». La normalisation se démontre à l’aide de relations logiques. Cependant, les systèmes de types imprédicatifs comme le système F débouchent facilement sur des relations logiques mal définies car circulaires. La technique des « candidats de réductibilité » de Girard évite cette circularité.
Du système F à Coq et Agda, le chemin est long et passe par l’ajout de types dépendants, d’opérateurs de types, de types inductifs ou coinductifs, et d’une hiérarchie d’univers. Des fragments significatifs de la logique de Coq ont été formalisés et vérifiés en Coq, parfois en démontrant la normalisation, souvent en l’admettant. De même, des fragments d’Agda ont été formalisés en Agda en suivant une approche de syntaxe intrinsèquement typée.
Arriverons-nous un jour à « vérifier Coq en Coq », c’est-à-dire à montrer la cohérence logique de Coq par une démonstration mécanisée en Coq ? Le second théorème d’incomplétude de Gödel nous dit que c’est impossible à strictement parler. Mais il semble plausible que l’on puisse vérifier un grand fragment de Coq ou d’Agda en utilisant un fragment à peine plus grand, ce qui constituerait un magnifique « auto-amorçage » de ces assistants à la démonstration.
