Journal Sémantiques mécanisées : quand la machine raisonne sur ses programmes.

Depuis l'an dernier, Xavier Leroy est le nouveau titulaire de la chaire « sciences du logiciel » au Collège de France. J'en avais fait un journal pour présenter le thème de sa première année de cours où il abordait la correspondance entre programmes et démonstrations mathématiques, connue sous le nom de correspondance de Curry-Howard.

Cette année, il a décidé d'aborder la formalisation de la sémantique des langages de programmation avec l'aide de la machine (en utilisant l'assistant de preuve Coq). On pourra trouver le programme de l'année sur le site du Collège de France :

« 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 présentera 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 seront entièrement mécanisées avec l'assistant Coq. Cependant, une grande partie du cours restera accessible sans connaissance préalable de Coq. Le séminaire approfondira l'approche dans plusieurs directions, allant de la mécanisation des « gros » langages comme Javascript et Rust à l'utilisation d'assistants à la démonstration pour enseigner les fondements des langages de programmation.

Les cours ont commencé jeudi dernier et se tiendront tous les jeudis jusqu'à début février (sauf ce jeudi, le cours étant annulé suite au mouvement de grève pour la réforme des retraites). On peut ensuite les retrouver au format audio (dès le lendemain) ou vidéo (quelques jours plus tard, celui de jeudi dernier est disponible depuis hier lundi) sur la page du cours accompagnés du pdf de la présentation.

Mais, chose exceptionnelle et même une première pour cet institut, les cas pratiques étudiés ont leur dépôt github pour ceux qui voudrait jouer avec. Xavier Leroy y traitera la formalisation et l'implémentation de deux langages simples, l'un impératif et l'autre fonctionnel statiquement typé.

Parmi les séminaires qui suivent l'enseignement, on trouvera, entre autres, Philip Wadler (auteur des types classes de Haskell ou des génériques en Java) parlant de l'utilité des assistants de preuve pour enseigner la théorie des langages de programmation, ou d'autres intervenants sur l'usage des méthodes de sémantiques formelles pour étudier des langages comme javascript ou rust.