Xavier Leroy, élu à l’Académie des sciences : une vie dédiée à l’informatique

Une appétence précoce pour l’informatique

Aux yeux de nombre de ses collègues chercheurs en mathématiques et en informatique, en France comme à l’étranger, la carrière de Xavier Leroy, est en tout point remarquable. Les prestigieux prix scientifiques qui lui ont été décernés dans la décennie passée témoignent de sa créativité d’informaticien et de ses talents de programmeur, à l’origine de contributions majeures au développement des méthodes formelles et des langages fonctionnels.

Xavier Leroy s’est également illustré par son engagement constant à développer la science informatique et à la représenter au-delà du cercle de ses initiés. Ce brillant parcours de chercheur s’enrichit désormais d’une nouvelle reconnaissance, avec son élection récente à l’Académie des sciences.

Des rencontres scientifiques décisives

La carrière de Xavier Leroy est jalonnée de rencontres qui ont façonné son cheminement d’informaticien visionnaire. La première d’entre elles a eu lieu au milieu des années 1980, lors de la visite d’un laboratoire de physique théorique à l’Université d’Orléans, alors qu’il est lycéen. Il garde un souvenir mémorable de ce premier échange avec des scientifiques. L’adolescent se passionne déjà pour les sciences et l’informatique, dont il découvre les principes en « bidouillant » ses premiers programmes sur un ordinateur individuel, comme beaucoup d’autres jeunes alors.

À l’École normale supérieure qu’il intègre en 1987, Xavier Leroy fait ses premiers pas en informatique : « Les mathématiques à l’ENS étaient la voie royale, mais je les trouvais difficiles… et je me suis orienté vers l’informatique. Les cours d’algorithmique, de calcul symbolique ou de programmation, m’ont, tout autant que les mathématiques, séduit par leur richesse et leur rigueur scientifique », se rappelle le chercheur.

Sa carrière débute par un stage de première année chez Inria, sous la houlette de Guy Cousineau, dédié à la découverte du langage de programmation fonctionnelle Caml : 

L’institut était déjà à l’époque très en avance sur le numérique, avec des équipements de pointe et des chercheurs précurseurs de ces sciences.

Un investissement sans faille dans la recherche

Après un DEA, Xavier Leroy se lance dans une thèse en informatique sous la direction de Gérard Huet, grand nom de la discipline. En 1993, son doctorat en poche, il rejoint l’Université de Stanford pour deux ans de postdoctorat :

J’ai eu la chance de rencontrer des pionniers de l’informatique, en pleine Silicon Valley, dans un campus doté de moyens exceptionnels – une expérience inoubliable ! Une fois rentré en France, il était évident que l’Inria était le bon endroit pour mener mes recherches…, confie-t-il.

Il rejoint donc l’institut en 1994 en tant que chargé de recherche et y développe et perfectionne le langage Caml, qui deviendra ensuite OCaml. Production phare d’Inria, OCaml est le support de développement de nombreux logiciels, utilisés en recherche – par exemple l’assistant de preuve Coq, précieux allié du raisonnement des mathématiciens – ou dans l’industrie. « La mise au point d’OCaml a été le projet de nombreuses années, résume Xavier Leroy. Distribué en 2022 dans sa version 5.0, il est accessible en open source et permet de développer des applications informatiques avec de très hautes garanties de sûreté et de fiabilité. Après avoir été utilisé pour l’industrie (aéronautique, spatial, nucléaire), il s’avère de nos jours très prisé pour des applications aux systèmes, à la blockchain, ou à l’informatique financière. »

Une diversité d’expériences en recherche et enseignement

Fin 1990, Xavier Leroy s’intéresse aux questions de sécurité informatique et rejoint pour quelques années la startup Trusted Logic, spécialisée dans ce domaine. Aux côtés de Dominique Bolignano, son fondateur, il en sera le conseiller scientifique : « Âgé de 32 ans à l’époque, j’étais l’un des seniors d’une équipe au sein de laquelle dynamisme et créativité étaient de mise ! ».

Revenu chez Inria après la vente de Trusted Logic en 2002, Xavier Leroy travaille avec Sandrine Blazy à la conception et la vérification formelle d’un compilateur pour le langage C, CompCert. Les performances de fiabilité de ce compilateur, démontrées mathématiquement, en ont progressivement fait un outil d’intérêt académique comme industriel – en particulier pour le développement de programmes critiques dans des industries sensibles (aéronautique, nucléaire).

Ces projets majeurs sont unanimement salués par ses pairs, Xavier Leroy recevant nombre de distinctions, avant d’être nommé, en 2018, professeur au Collège de France. Il y est titulaire de la chaire permanente "Sciences du logiciel", comme Gérard Berry, son illustre prédécesseur. « C’est un immense honneur que de porter la voix de l’informatique dans l’une des plus anciennes institutions françaises, souligne-t-il. Le Collège de France est aussi très novateur, proposant tous ses cours en ligne, comme la traditionnelle leçon inaugurale. Transmettre son savoir à destination du plus grand nombre est très gratifiant, mais demande aussi beaucoup de travail, car il est demandé de dispenser chaque année des cours originaux… »

La reconnaissance d’une carrière exemplaire

Partageant son temps entre l’enseignement au Collège de France et la recherche chez Inria, où il reste membre de l’équipe Cambium, Xavier Leroy a été surpris par son élection à l’Académie des sciences.

Je ne m’y attendais pas, cet événement est évidemment un grand honneur, mais je suis surtout fier de représenter l’informatique, à la suite de la première génération de ses pionniers français, comme Gérard Huet, Gérard Berry ou Serge Abiteboul. L’informatique est maintenant reconnue comme une discipline scientifique à part entière et je ne peux que m’en réjouir !

Avec cette élection, Xavier Leroy souhaite assumer le rôle d’ambassadeur de l’informatique et faire valoir l’originalité de sa discipline. L’informatique, c’est évidemment une technique, dont les applications se sont immiscées dans le quotidien des entreprises et des citoyens, et qui a permis le développement de pans entiers de notre économie. Mais c’est aussi une science, composée de savoirs fondamentaux – programmation, langages, données, etc. –, s’appuyant sur des concepts rigoureux et nécessitant des connaissances en perpétuelle évolution.

Cette élection à l’Académie des sciences, loin de signer la fin de sa carrière, marque pour le chercheur le début d’une nouvelle ère :

Je compte m’investir encore sur des questions ouvertes en informatique et en défendre l’intérêt. La dimension scientifique de la discipline, moins connue du grand public ou des décideurs du monde économique et politique, est essentielle aux progrès de ses techniques. Sans recherche théorique en informatique, nous ne pourrons pas compter sur des innovations futures, utiles à tous…

• Cambium dévoile une nouvelle version du langage de programmation OCaml, Inria, 16/12/2022.
• CompCert, un logiciel récompensé par une haute distinction, Inria, 29/6/2022.
• Le logiciel, entre l'esprit et la matière, leçon inaugurale de Xavier Leroy (vidéo), Collège de France, 15/11/2018.
• Xavier Leroy : Grand Prix – Académie des sciences, Inria, 29/10/2018.
• Avec Xavier Leroy, l’informatique confirme sa présence au Collège de France, Inria, 15/6/2018.
• Pourquoi créer des nouveaux langages de programmation ? Interstices, 28/01/2019.