Avec Xavier Leroy, l’informatique confirme sa présence au Collège de France

Quels ont été vos principaux axes de recherche chez Inria ? 

Que ce soit avec l’équipe Gallium créée en 2006 ou précédemment avec l’équipe Cristal, je me suis intéressé à ce qui peut rendre un logiciel plus fiable ou de meilleure qualité. Nous avions en premier lieu une approche focalisée sur les langages de programmation pour les rendre plus expressifs, plus sûrs, plus simples. L’un de nos résultats visibles est le langage de programmation OCaml , qui a connu un certain succès.

À la création de Gallium, nous avons souhaité étendre le périmètre de nos recherches en travaillant sur la preuve de programmes - c’est-à-dire la manière dont on peut démontrer mathématiquement la fiabilité d’un logiciel - et plus particulièrement des compilateurs. Dans nos travaux, nous utilisons d’ailleurs des technologies issues d’Inria telles que l’assistant de preuves Coq. Cela a donné naissance au projet Compcert, premier compilateur réaliste qui a été vérifié mathématiquement.

Que représente pour vous cette nomination au Collège de France ?

Être nommé dans une telle institution est pour moi un très grand honneur. Mais il s’agit aussi d’une reconnaissance pour la discipline. Le système universitaire français a en effet mis du temps à reconnaître l'informatique - 20 à 30 ans après les États-Unis ou le Royaume-Uni.

Au Collège de France, c’est Gérard Berry, issu d’Inria également, qui a ouvert la voie en faisant entrer l’informatique, d’abord sur deux chaires annuelles en 2007 et 2009, puis sur la chaire permanente "Algorithmes, machines et langages" à partir de 2012. Je suis très heureux de suivre la piste tracée par Gérard, qui prendra sa retraite prochainement. Pédagogue admirable, il a su se faire l’ambassadeur de la science informatique en partageant son enthousiasme et son savoir.

Je vois par ailleurs comme un autre très bon signe pour la discipline la création l’année dernière de la chaire de Stéphane Mallat, "Sciences des données". Nos deux enseignements pourront être très complémentaires dans leur approche des problématiques de l’informatique moderne.

Quels types de contenus souhaitez-vous enseigner ? 

J’essaierai d’expliquer les fondements des sciences du logiciel. C’est-à-dire quels sont les principes mathématiques permettant de raisonner, construire et vérifier des logiciels, des langages ou des outils de programmation. Je souhaite montrer la rigueur mathématique qu’il est possible d’insuffler dans toutes les activités autour du logiciel.

Je souhaiterais ainsi présenter l’histoire des idées pour faire comprendre comment certains concepts sont apparus, mais aussi et surtout rendre compte de la recherche contemporaine, la science "en train de se faire". Par exemple, en présentant certaines avancées opérées ces dix dernières années qui permettent à des idées d’abord fondamentales de devenir désormais utilisables par des industriels. Ou encore tout ce qui tourne autour de l’apprentissage machine ou machine learning . Cela change complètement la donne. Certains logiciels de nos jours ne sont plus vraiment écrits, mais plutôt appris à partir d’exemples. Comment alors raisonner dessus ou assurer leur fiabilité ? J’aimerais ouvrir ces pistes de réflexion dans mon enseignement.

Et concernant le style de vos cours ?

Enseigner au Collège de France n’est pas comme faire cours en master. Les cours y sont ouverts à tous, tant sur place qu’en ligne, et l’auditoire est très diversifié, du grand public aux chercheurs spécialistes du domaine.

Il n’est donc pas aisé de trouver la combinaison idéale entre la technicité du savoir et son accessibilité pour pouvoir communiquer quelques intuitions simples et attirer de nouvelles personnes vers la discipline. C’est d’ailleurs un point sur lequel j’ai eu la chance d’échanger avec l’ensemble des professeurs du Collège de France lors de ma candidature. Pour moi, ce sera l’un des challenges à relever lors de la leçon inaugurale prévue mi-novembre puis lors de mes cours qui se prolongeront jusqu’à fin janvier.