Xavier Leroy : Grand Prix – Académie des sciences

Comme beaucoup, c'est dans sa chambre d'adolescent que Xavier Leroy a fait connaissance avec l'informatique. « C'était alors le début des ordinateurs individuels et leurs capacités étaient pour le moins limitées… mais je me souviens que j'essayais d'écrire de petits programmes. C'était amusant, mais surtout frustrant… » Le coup de foudre viendra plus tard, en première année à Normale Sup', avec la découverte de l’informatique fondamentale, un univers passionnant et d'une grande pureté formelle. Après un stage dans la Silicon Valley il rejoint l'équipe Formel commune à l’ENS et à Inria Rocquencourt le temps d'une thèse sur les systèmes de types des langages de la famille ML, avant de retourner aux États-Unis, cette fois-ci à Stanford pour un postdoctorat.

De CAML à Caml Light à OCaml

« En 1994 j'ai intégré Inria "pour de bon" en étant recruté par l'équipe Cristal – toujours à Rocquencourt -  pour poursuivre mes recherches sur les langages de programmation fonctionnelle. » Ces travaux avaient débuté par une implémentation légère mais très efficace du langage Caml, appelée Caml Light, qui a permis au langage de se répandre, notamment en France pour l’enseignement de la programmation. « Progressivement, il a pris de l'envergure et évolué vers un langage très complet nommé OCaml, désormais utilisé dans la recherche ainsi que chez de nombreux industriels, dans la finance, la sécurité, le Web, etc. »

Sur la piste du zéro-défaut…

À la fin des années quatre-vingt-dix, Xavier Leroy élargit ses horizons et s'intéresse de plus près au rôle que peuvent avoir les langages de programmation dans la sécurité informatique. Des investigations qui l'amènent à contribuer à la création d'une startup spécialisée dans la sécurisation des cartes à puces (Trusted Logic) avec laquelle la collaboration durera cinq ans. "En 2004, de retour à 100% chez Inria mais fort de ce que j'avais appris chez Trusted Logic j'ai plongé dans le monde des méthodes formelles avec, en ligne de mire, la vérification des logiciels critiques comme ceux qui équipent les cartes à puces mais aussi les commandes électroniques des avions, les métros sans conducteurs ou encore la régulation des centrales nucléaires. " À la tête de son équipe – devenue Gallium en 2006 -  Xavier Leroy concentre alors ses recherches sur la vérification formelle des compilateurs, ces programmes chargés de traduire un code source écrit dans un langage de programmation de haut niveau en langage machine et qui, à ce titre, sont des rouages essentiels de la chaîne de sécurisation des logiciels critiques. Car de même qu’un contresens dans une traduction entre langues naturelles change le sens d’un texte, un bug dans un compilateur peut le conduire à produire un code machine ne respectant pas les intentions exprimées dans le programme source.  

CompCert : un jalon de la vérification formelle des compilateurs

« C'est ainsi que nous avons créé CompCert, un compilateur pour le langage C couramment utilisé pour les logiciels critiques. Son point fort : il assure que chaque passe de compilation a fait l'objet d'une preuve mathématique qui garantit que la sémantique du programme est préservée. Pour ce faire il utilise l'assistant de preuve Coq, issu d'Inria. » En 2011, une étude par test aléatoire a comparé CompCert et les principaux autres compilateurs C. Et alors que des centaines de bugs ont été identifiés sur ses concurrents, CompCert a affiché un sans-faute…. Rien d'étonnant à ce que l'outil made in Inria ait rencontré un grand intérêt académique et redynamisé la recherche en vérification formelle des compilateurs…« Chez les industriels aussi l'intérêt grandit. Il y a quelques années nous avons signé un partenariat de commercialisation avec Absint, une PME allemande et aujourd'hui nous avons un premier utilisateur industriel en la personne de MTU, une entreprise qui fabrique des composants pour le nucléaire sachant qu'Airbus étudie de près la possibilité d'utiliser CompCert pour certains de ses logiciels embarqués… »

Nouveau départ, nouveaux champs de recherche

Très fier du succès d’OCaml et de CompCert, Xavier Leroy entre aujourd'hui dans une nouvelle étape de sa vie, avec sa nomination au Collège de France sur la chaire permanente "sciences du logiciel". Hasard du calendrier, ce grand prix Inria – Académie des Sciences arrive donc au moment où Xavier Leroy s’apprête à prendre de la distance avec un institut où il aura passé l'essentiel de sa vie de chercheur : « Je dois beaucoup à Inria qui a su soutenir nos travaux dans la durée sans exiger une rentabilité à court terme. Je veux voir dans ce prix un signe que la recherche "au long cours" en informatique de base a encore sa place chez Inria ! » Mais ces activités professorales n'empêcheront pas Xavier Leroy de poursuivre ses recherches.  « En préparant ma leçon inaugurale, je me suis rendu compte que j'avais envie de renouer avec d’autres territoires de recherches, résume-t-il en conclusion. Je voudrais aujourd'hui explorer de nouvelles thématiques comme les langages pour mieux programmer le hardware massivement parallèle, ou encore l'évolution de la vérification formelle à l'heure du deep learning : comment ferons-nous pour vérifier un logiciel qui n'est plus entièrement écrit mais en partie appris ? Mais je souhaite aussi prendre le temps de m'intéresser aux questions d'éthique, en particulier aux menaces que pourrait faire peser le numérique sur les libertés individuelles et sur les processus démocratiques… C'est un sujet qui me concerne en tant que scientifique, mais aussi en tant que citoyen ! »