🗣 Guillaume Andrieu Jean-Yves Girard, le génial inventeur des indispensables montres à moutarde (1990), est certes un joyeux trublion. Mais avant d’en arriver à ce sommet indépassable, il a tout de même publié deux-trois petites choses en chemin: Rust, vous connaissez? L’idée première du système de typage de Rust est la logique dite “linéaire”, due à Jean-Yves Girard (1987). Haskell, ça vous dit quelque chose? Les systèmes de typage de Haskell mais aussi Scala (et d’une certaine manière Java) sont basés sur le “système F” (ou lambda-calcul de second ordre), dû à… Jean-Yves Girard (1972). Idris, vous avez entendu parler? Le système de typage d’Idris est basé sur la théorie des types de Per Martin-Löf, dont la première version a été prouvée incorrecte par… Jean-Yves Girard, qui depuis possède un paradoxe à son nom. (Girard et Martin-Löf sont par ailleurs de très bons potes et ont ferraillé sec contre les logiciens classiques dans leur prime jeunesse.) Très méconnu mais probalement l’un des penseurs les plus influents pour l’informatique de ce début de XXIe siècle, Girard est tout aussi sérieux que fantasque. Son style toujours acéré et polémique s’appuie sur une vision très claire de ce que devrait être la logique: vivante, joyeuse, fertile. Dans cette courte présentation, on s’attachera à comprendre pourquoi Girard est aussi virulent dans son discours, quels sont les objectifs de sa pensée, et pourquoi elle a déjà porté tant de fruits dans le monde de l’informatique.