La leçon inaugurale a rappelé les liens historiques entre logique et informatique. Le cours 2018-2019 de la chaire Sciences du logiciel a étudié un autre lien, de nature mathématique celui-là (il s’agit d’un isomorphisme), entre langages de programmation et logiques mathématiques. Dans cette approche, démontrer un théorème, c’est la même chose que d’écrire un programme ; énoncer le théorème, c’est la même chose que de spécifier le type du programme.
Cette correspondance entre démonstration et programmation a d’abord été observée dans un cas simple par deux logiciens : Curry en 1958, puis Howard en 1969. Le résultat semblait tellement anecdotique que Howard ne l’a jamais soumis à une revue, se contentant de faire circuler des photocopies de ses notes manuscrites. Rarement photocopie a eu un tel impact scientifique, tant cette correspondance de Curry-Howard est entrée en résonance avec le renouveau de la logique et l’explosion de l’informatique théorique des années 1970 pour s’imposer dès 1980 comme un lien structurel profond entre langages et logiques, entre programmation et démonstration.
Aujourd’hui, il est naturel de se demander quelle est la « signification logique » de tel ou tel trait de langage de programmation, ou encore quel est le « contenu calculatoire » de tel ou tel théorème mathématique (c’est-à-dire, quels algorithmes se cachent dans sa démonstration ?). Plus important encore, la correspondance de Curry-Howard a débouché sur des outils informatiques comme Coq et Agda, qui sont à la fois des langages de programmation et des logiques mathématiques, et s’utilisent aussi bien pour écrire et vérifier des programmes que pour énoncer et aider à démontrer des théories mathématiques.
Le cours a retracé ce bouillonnement d’idées à la frontière entre logique et informatique, et mis l’accent sur les résultats récents et les problèmes ouverts dans ce domaine. Le séminaire a donné la parole à sept experts du domaine pour des approfondissements et des points de vue complémentaires.