À propos des compilateurs

Un compilateur est un programme informatique qui transforme un code source écrit dans un langage de programmation (le langage source) en code de bas niveau (le langage cible, compréhensible par la machine). Le compilateur effectue donc une traduction en quelque sorte.

A priori, le compilateur produit un code qui se comporte comme le programme source dont il est issu. Mais il est difficile d’être sûr que le compilateur préserve la sémantique des programmes, et donc que la traduction effectuée est correcte. Aussi, il arrive parfois que des erreurs soient introduites lors de la compilation. Pour la plupart des logiciels, les conséquences sont rarement dramatiques. Pour les logiciels critiques par contre, cela peut être plus grave. Le maillon faible de la chaîne reste donc le compilateur…

CompCert est un compilateur réaliste du langage C vérifié formellement. Comme nous l’explique Sandrine Blazy, sa particularité est d’être accompagné d’un théorème de préservation sémantique. Elle nous précise l’intérêt de ce théorème qui fait de CompCert le premier compilateur garanti « zéro faute ».