LE DIRECT
Extrait du code du langage générique de programmation, OCaml

Le Logiciel entre l’esprit et la matière, leçon Inaugurale de Xavier Leroy

59 min
À retrouver dans l'émission

Entre "rigueur formelle et créativité débridée", quelle est l'ampleur des progrès dans le monde du logiciel depuis l'apparition de l’ordinateur? Le logiciel serait-il juste de la logique qui s'exécute? L’informaticien Xavier Leroy analyse comment le logiciel pourrait être l'incarnation de la logique

Extrait du code du langage générique de programmation, OCaml
Extrait du code du langage générique de programmation, OCaml Crédits : OCaml

De quelle façon le problème central du logiciel peut-il se déplacer du fait « de programmer » à celui de « convaincre »? »  Pourquoi avons-nous plus que jamais besoin de la rigueur mathématique? Demande encore Xavier Leroy. 

Informaticien spécialiste des langages et outils de programmation, titulaire de la chaire Sciences du logiciel au Collège de France, Xavier Leroy nous invite, selon sa formule à « un bouillonnement d'idées à la frontière entre logique et informatique… » dans sa leçon inaugurale. 

Couronné de nombreux prix, le parcours de Xavier Leroy est riche et brillant comme le rappelle sa présentation sur les sites du Collège de France et de l’INRIA

"Formé aux mathématiques et à l'informatique à l'École normale supérieure, puis à l'INRIA où il a effectué sa thèse, il est passé par l’université de Stanford pour son post- doctorat. Devenu chargé de recherche à l’Inria en 1994, puis directeur de recherche en 2000, il a dirigé l’équipe de recherche GALLIUM. De 1999 à 2004, il également participé à la start-up Trusted Logic."

"Programmeur prodige », comme le rappelle ses pairs, "il s'est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujourd'hui OCaml, l'un des deux langages fonctionnels typés les plus utilisés au monde, dans des domaines aussi divers que l'aéronautique, la finance ou encore le Web". 

"Ce langage est le support de développement d'outils logiciels très variés comme l'assistant de preuve Coq"que nous allons croiser aujourd’hui. 

"OCaml a été utilisé dans de nombreux projets emblématiques comme la version web de Facebook Messenger, le logiciel MediaWiki ou encore l'infrastructure de virtualisation Docker."

Dans cette passionnante et stimulante leçon inaugurale, Xavier Leroy propose de revenir « sur les concepts fondamentaux de la programmation et l'histoire de leur apparition ». 

"Ce n'est pas dans le calcul numérique qu'il faut chercher la racine, dit-il aujourd’hui, mais dans une toute autre branche des mathématiques, à la frontière avec la philosophie : la logique"

Xavier Leroy, lors de sa leçon inaugurale au Collège de France (capture d'écran)
Xavier Leroy, lors de sa leçon inaugurale au Collège de France (capture d'écran) Crédits : Collège de France

Xavier Leroy rappelle :

"l 'explosion de l’informatique doit beaucoup aux immenses progrès de la micro-électronique, qui débouche sur la production de masse d’ordinateurs et de systèmes sur puce toujours plus puissants à coût constant, mais aussi à l’incroyable flexibilité du logiciel qui s’exécute sur ces systèmes. Reprogrammable à l’infini, dupliquable à coût zéro, libéré de presque toute contrainte physique, le logiciel peut atteindre une complexité invraisemblable."

Mais le "revers de cette flexibilité, souligne-t-il, c’est le logiciel qui est aussi extrêmement vulnérable aux erreurs de programmation : les bugs tant redoutés…"

Xavier Leroy, qui "est à l’origine de  CompCert, compilateur C certifié, qui  autorise une vérification formelle d’une taille et d’une complexité  sans précédent (la certification et la vérification automatique des chaînes logicielles qu'il permet ont fait progresser la programmation 'zéro défaut') indique dans sa leçon inaugurale :

"Si le comportement d'un programme C peut-être connu avec la précision des mathématiques, comment se fait-il que ce comportement soit si souvent erratique, entre (bugs) plantages et failles de sécurité" ? 

Quelle est alors la problématique de la vérification formelle du logiciel? Comment spécifier ce que le programme est censé faire? 

Que voulons-nous ? Est-il conforme aux attente de l'utilisateur? avons-nous écrit le bon programme? En s’inscrivant dans une histoire où l’on croise Leibniz, Hilbert et bien sûr les Lovelace et Turing, jusqu’aux dernières innovations qui touchent l’Intelligence Artificielle, Xavier soulève bien des questions passionnantes

Nous gagnons le Collège de France, le  15 novembre 2018, pour la Leçon Inaugurale de Xavier Leroy, intitulée "Le Logiciel entre l’esprit et la matière".

Pour prolonger :

La leçon Inaugurale de Xavier Leroy est publiée sous le titre Le Logiciel entre l’esprit et la matière. Chez Fayard

Intervenants
  • Informaticien, professeur au Collège de France, titulaire de la chaire Sciences du logiciel
L'équipe

France Culture

est dans l'appli Radio France
Direct, podcasts, fictions

INSTALLER OBTENIR

Newsletter

Découvrez le meilleur de France Culture

S'abonner
À venir dans ... secondes ...par......