Quelle confiance accorder à un compilateur? Comment savoir que le code machine produit se comporte comme prescrit par la sémantique du programme source? La question est particulièrement importante pour le logiciel critique, dont le code source est certifié à l'aide de méthodes formelles, et pour lesquels tout bug dans le compilateur peut invalider la certification.
Plusieurs solutions à ce problème ont été proposées, notamment le code auto-certifié (proof-carrying code) et la validation de traducteurs. L'approche la plus directe est la certification formelle du compilateur lui-même, vu comme un programme critique: on cherche à prouver sur machine un résultat de préservation de la sémantique entre le code source fourni et le code machine produit.
Avec l'aide des membres de l'ARC Concert, j'ai réalisé une telle preuve, en Coq, d'un back-end de compilateur modérément optimisant, qui traduit Cminor (un langage intermédiaire impératif de bas niveau) en assembleur PowerPC. Une originalité de ce travail est que l'essentiel du compilateur est programmé directement dans le langage de spécification de Coq, puis extrait automatiquement vers du code Caml exécutable. L'exposé présentera une vue d'ensemble de ce compilateur et de sa (très grosse) preuve en Coq, et tirera quelques leçons de cette expérience.