Les Newsletters Interstices
    Niveau facile
    Niveau 1 : Facile

    À propos des compilateurs

    Langages, programmation & logiciel
    Sécurité & Vie privée
    Peu connue des non-informaticiens, la compilation est pourtant un des fondements de la programmation. Sandrine Blazy nous présente le rôle des compilateurs dans cet épisode du podcast audio.

    Écoutez l'interview de Sandrine Blazy

    Sandrine Blazy

    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 ».

    Newsletter

    Recevez chaque mois une sélection d'articles

    Niveau de lecture

    Aidez-nous à évaluer le niveau de lecture de ce document.

    Si vous souhaitez expliquer votre choix, vous pouvez ajouter un commentaire (Il ne sera pas publié).

    Votre choix a été pris en compte. Merci d'avoir estimé le niveau de ce document !

    Sandrine Blazy

    Professeur à l'Université de Rennes 1, membre de l'équipe CELTIQUE.
    Voir le profil

    Joanna Jongwane

    Rédactrice en chef d'Interstices, Direction de la communication d'Inria
    Voir le profil