Derrière “l'affreux informaticien qui est tout le temps en retard”, se cache un scientifique au calme olympien. Informaticien autodidacte, il a trouvé son équilibre entre théorie et pratique. Rencontre avec Gabriel Scherer, nouveau chargé de recherche à l'IRIF.

Tout le jeu est de comprendre comment formaliser des propriétés qui intuitivement sont importantes pour les programmeurs et les programmeuses (quand on utilise mon langage, le problème X ou Y ne va jamais arriver), et réfléchir à comment les rendre vraies et prouver qu'elles sont vraies. Gabriel Scherer, chargé de recherche | Pôle Preuves, programmes et systèmes - Équipes Algèbre et calcul, Analyse et conception de systèmes et Preuves et programmes

Quand j'étais petit je voulais devenir (astronaute, cuisinier, puis) mathématicien. J'avais envie de faire des choses intéressantes et jolies, et de travailler pour l'intérêt général. J'ai découvert la programmation au lycée, mon prof de maths m'a envoyé au club informatique local, et j'ai adoré. J'ai ensuite approfondi de mon côté, avec les ressources qu'on pouvait trouver sur internet à l'époque.
Pendant mes études, j'ai graduellement glissé des mathématiques, domaine fascinant mais aussi très exigeant, vers une partie de l'informatique autour de la programmation, que je trouvais plus directe et plus facile.

Pendant ma formation j'ai été à l'ENS et au MPRI, en thèse à l'INRIA Rocquencourt pendant quatre ans, et en post-doc à l'université Northeastern à Boston pendant un an et demi. J'avais déjà une idée précise de quels domaines me plaisaient et de sur quoi j'avais envie de travailler, ce qui aide à faire des choix.

Le post-doc aux États-Unis a été une période difficile, peut-être ma première vraie expérience de difficulté professionnelle. Ce qui m'a frappé c'est la façon, quand les choses vont mal et qu'on ne sait pas forcément pourquoi, qu'on a de toute suite penser que c'est de notre faute, d'internaliser et de se pourrir la vie avec ces difficultés.

Je travaille sur les langages de programmation, en théorie et en pratique. Ma communauté scientifique étudie les programmes et les langages de programmation comme des objets formels, sur lesquels on peut faire des mathématiques. Tout le jeu est de comprendre comment formaliser des propriétés qui intuitivement sont importantes pour les programmeurs et les programmeuses (quand on utilise mon langage, le problème X ou Y ne va jamais arriver), et réfléchir à comment les rendre vraies et prouver qu'elles sont vraies.

On peut travailler sur des langages existants, pour mieux les comprendre ou pour améliorer; en modifiant le langage, ou en écrivant des outils au-dessus pour repérer certains dangers. Mais c'est compliqué car les langages sont gros et complexes, les étudier formellement est difficile, et faire accepter des changements à leur communauté est énormément de travail technique et social. On peut aussi se concentrer sur des langages “jouets” ou “noyaux” pour aller au cœur du problème qui nous intéresse dans un cadre simplifié, épuré, mais plus éloigné de la pratique.

L'idée clé est de capturer des propriétés d'utilisabilité des langages comme des énoncés mathématiques : normalisation, confluence, sûreté, etc. Ce domaine est une forme de maths qui n'est pas très clairement reliée au corpus central de mathématiques, on utilise assez peu d'outils mathématiques avancés.

Côté pratique, je fais partie de l'équipe de développeurs du langage OCaml, qui font évoluer le langage et son implémentation. C'est beaucoup de travail de développement avec parfois des questions de recherches qui apparaissent. C'est un logiciel libre avec un développement collaboratif et assez actif (des dizaines de messages par jour dans des discussions en parallèle), un mode de travail qui est prenant mais très chronophage.

De l'activité de programmation, qui est fascinante. Quand on programme des choses intéressantes, on se sent très créatif, c'est scotchant. Ça donne envie d'améliorer encore les outils que l'on utilise pour programmer, les langages de programmation, pour nous aider à encore mieux exprimer nos intentions, à l'ordinateur et auprès de nos collègues qui travaillent sur le même programme.

Les membres de l'IRIF connaissent mieux que moi les aspects mathématiques de mon domaine, les outils avancés qui peuvent donner une perspective théorique sur la conception de langages de programmation. J'espère apprendre par osmose.

C'est aussi un des lieux de développement de l'assistant de preuve Coq, un logiciel fascinant : c'est un langage de programmation et de preuve, pour écrire des programmes et des preuves mathématiques. J'aimerais bien mettre un peu les mains dans le cambouis et comprendre mieux comment il est fait à l'intérieur.

J'ai un poste idéal dans un chouette endroit, alors le but pour l'instant est de ne pas trop changer. Le point clé en temps que semi-jeune est l'encadrement d'étudiant et d'étudiantes. C'est plus compliqué que travailler tout seul, mais c'est aussi plus social, on découvre des gens et on aide à les former, c'est très gratifiant ! J'ai travaillé avec des stagiaires et un étudiant en thèse, Olivier. J'espère continuer en travaillant avec d'autres personnes, à dose raisonnable.

L'année dernière, pendant la mobilisation contre la réforme des retraites, le centre de loisirs où va mon fils de 4 ans était en grève un jeudi, alors je l'ai emmené voir l'incinérateur d'Ivry et ensuite les bureaux de l'IRIF. « Tu vas voir comment les gens travaillent ici, comme ton papa. » On est tombé sur le Cake de l'IRIF. Il a adoré !

En ce moment, ce qui mange tout mon temps hors-travail, ce sont mes deux fils: Lucien, 5 ans et Camille, 2 ans et demi. C'est très rigolo de s'occuper de jeunes enfants; je peux leur faire des grands discours pour répondre à leurs nombreuses questions et on s'amuse bien. Camille ne fait toujours pas ses nuits, je suis donc en mode zombie la plupart du temps, avec une compréhension des choses et une mémoire au ralenti.

2023 : Mutation dans l'équipe PiCube de l'INRIA Paris, localisée à l'IRIF.
2017-2023 : Chargé de recherche à l'INRIA Saclay dans l'équipe Partout, qui fait de la théorie de la démonstration et des langages de programmation.
2016-2017 : Post-doc à Northeastern (Boston, USA) avec Amal Ahmed, sur les sémantiques multi-langages.
2012-2016 : Thèse à l'INRIA Rocquencourt avec Didier Rémy, “Quels types simples ont un habitant unique ?”.