Sémantiques mécanisées : quand la machine raisonne sur ses langages

« Que fait ce programme, au juste ? » Pour répondre à cette question avec la précision des mathématiques, il nous faut une sémantique formelle du langage dans lequel ce programme est écrit. Plusieurs approches de la sémantique formelle sont bien maîtrisées aujourd’hui : sémantiques dénotationnelles, qui interprètent le programme comme un élément d’une structure mathématique ; sémantiques opérationnelles, qui décrivent les étapes successives des exécutions du programme ; sémantiques axiomatiques, qui décrivent les assertions logiques satisfaites par ces exécutions. Ces sémantiques formelles ont de nombreuses applications : non seulement définir les langages de programmation avec une précision bien plus grande qu’un manuel de référence écrit en français ou en anglais, mais aussi vérifier la correction des algorithmes et des outils qui opèrent sur les programmes, comme les compilateurs, les analyses statiques, et les logiques de programmes.

La sémantique d’un langage de programmation peut être volumineuse et complexe, rendant les démonstrations « sur papier » utilisant ces sémantiques pénibles et peu fiables. Mais nous pouvons nous adjoindre l’aide de l’ordinateur ! Les assistants à la démonstration (Coq, HOL, Isabelle, etc.) fournissent un langage rigoureux pour définir les sémantiques, énoncer leurs propriétés, écrire des démonstrations, et vérifier automatiquement la cohérence de ces démonstrations. Cette mécanisation est un puissant levier pour faire passer les approches sémantiques à l’échelle des langages et des outils de programmation réalistes.

Le cours a présenté cette approche de sémantique mécanisée sur l’exemple de petits langages impératifs ou fonctionnels, avec des applications aux logiques de programmes et à la vérification de compilateurs et d’analyseurs statiques. Toutes ces notions ont été entièrement mécanisées avec l’assistant Coq. Le développement Coq est disponible à l’adresse https://github.com/xavierleroy/cdf-sem-meca.

Le séminaire a approfondi l’approche dans plusieurs directions, allant de la mécanisation de langages « du monde réel » comme Javascript et Rust à l’utilisation d’assistants à la démonstration pour enseigner les fondements des langages de programmation.