Paul De Brem : Commençons avec vous, Roberto Di Cosmo, professeur d’informatique à l’université de Paris Cité, vous êtes détaché auprès de l’Inria pour vous occuper justement de logiciels, de softwares. Vous est les fondateur et président de Software Heritage.
Si vous voulez bien, on va plutôt commencer par Mihalea, on va changer.
Professeur d’université en informatique à l’ENS Paris-Saclay, membre du laboratoire méthodes formelles et votre spécialité c’est la vérification des systèmes informatiques. Quand on vérifie les systèmes informatiques, d’abord on a vérifié le matériel, il y a des protocoles, et maintenant, de plus en plus, on vérifie les logiciels. D’abord historiquement on a vérifié les matériels. Pourquoi a-t-on vérifié les matériels plus que les protocoles et les logiciels ?
Mihaela Sighireanu : Merci pour l’introduction. Je suis très contente d’être ici avec vous.
Pourquoi a-t-on commencé par le matériel ? Tout simplement parce qu’à l’époque le matériel était simple. Il y avait des machines à états qu’on savait explorer, au moins qu’on savait énumérer, et parmi ces états on pouvait trouver des états où il y avait des bugs, des états qui n’étaient pas bons. Donc on a commencé par le matériel avec des méthodes formelles, c’est-à-dire des modélisations de ces matériels dans des structures mathématiques sur lesquelles, après, on savait raisonner, ces fameux invariants dont on parle depuis tout à l’heure. La France, à l’époque, était quand même pionnière dans ces méthodes. Il y a un eu un prix Turing à cette occasion-là et puis il y a des outils qui sont actuellement reconnus de manière internationale, qui ont justement des très bons résultats dans ces méthodes de vérification qu’on appelle la vérification basée sur les modèles.
Paul De Brem : Ce sont les matériels. Ensuite sont venus les protocoles.
Mihaela Sighireanu : Les mêmes outils ont été étendus après, je cite CADP [Construction and Analysis of Distributed Systems]mais d’autres outils ont été conçus à l’époque pour la vérification des protocoles, plutôt pour des invariants qui étaient, disons, finis, mais après aussi pour trouver des erreurs dans ces protocoles, surtout les protocoles de communication, c’est très important.
Paul De Brem : Maintenant, ce qui est apparemment très nouveau, c’est qu’on peut faire de la vérification du logiciel. C’est nouveau effectivement ?
Mihaela Sighireanu : Ce n’est pas si nouveau parce que ces méthodes ont été conçues dans les années 80. Les logiciels permettant de faire de la vérification ont mis un petit peu de temps à passer à l’échelle. Là je vais faire la fière pour notre communauté, parce que la France a eu aussi beaucoup d’impact dans ces technologies, dans ces techniques, ces méthodes. Je pense que la plupart des personnes dans la salle connaissent Coq [1] qui est un outil de modélisation mathématique, de certification des langages de programmation et de raisonnement sur ces langages de programmation. D’autres outils ont permis de faire de l’analyse automatique des programmes, je pense à l’outil Astrée.
Paul De Brem : Astrée, analyse de code embarqué sur Airbus, analyse du code sur le système de contrôle commande.
Mihaela Sighireanu : Tout à fait, qui est développé par des chercheurs français qui ont justement réussi à fiabiliser le logiciel qui tourne sur les Airbus, c’est extraordinaire.
Paul De Brem : Ça tombe bien. D’accord. C’est au point que maintenant on peut certifier les logiciels.
Mihaela Sighireanu : Voilà. Il y a eu la partie vérification automatique, mais cette vérification a ses limites, les limites données par tout ce qu’on apprend à nos étudiants sur la calculabilité en informatique. On peut franchir ces limites si un utilisateur humain aide le calculateur, l’outil de preuve. Là aussi on a des outils en France qui sont reconnus de manière internationale, je parle par exemple de Why3 [2], je parle des outils qui permettent de faire des vérifications du logiciel dirigées par l’humain au point qu’on est arrivé à vérifier des noyaux du système d’exploitation, des logiciels de taille importante qui ne sont pas faciles, pas forcément avec Why3 mais d’autres logiciels.
Paul De Brem : Vous utilisez le terme de révolution. Il y a eu une révolution il y a une dizaine d’années autour de la vérification des logiciels ?
Mihaela Sighireanu : Dès 2009/2010, on a vu des études de cas de passage à l’échelle important sur la vérification des logiciels. Je trouve que c’est quelque chose d’assez extraordinaire pour la fiabilité des logiciels.
Paul De Brem : Roberto Di Cosmo, vous vous intéressez aussi beaucoup aux logiciels, professeur d’informatique à Paris Cité. Vous êtes le fondateur et président de quelque chose qui s’appelle Software Heritage [3]. L’idée c’est d’archiver les codes sources de tous les logiciels publiquement disponibles. C’est une grande archive, un grand rassemblement si je puis dire. Combien de codes sources avez-vous réussi à recueillir de cette manière-là ?
Roberto Di Cosmo : Si vous regardez sur le site web du projet, qui est complètement ouvert, sur archive.softwareheritage.org [4], vous verrez qu’on a indexé à peu près 170 millions d’origines, ce qui ne veut pas dire 170 millions de projets différents car pas mal de copies du même projet sont éparpillées sur la planète. Ça fait à peu près 12 milliards de fichiers sources.
Paul De Brem : 12 milliards de fichiers sources !
Roberto Di Cosmo : Tout à fait, qu’on a récupérés.
Paul De Brem : D’accord, et qui sont répartis sur trois sites différents.
Roberto Di Cosmo : Oui. Je ne sais pas si vous voulez qu’on parle de toute la technologie qu’il y a derrière. On peut peut-être prendre un petit moment de hauteur là-dessus, un transparent est apparu là-derrière, peut-être deux secondes de réflexion parce qu’on a parlé beaucoup d’informatique, de l’origine de l’informatique, ses liens avec les mathématiques qui est un fondement fort ici en France, que j’ai toujours adoré et respecté. Vous entendez l’accent, bien que je sois là depuis 30 ans je suis quand même Italien ; quand je suis arrivé, j’ai trouvé fascinant le terreau de recherche qu’il y a ici. Depuis longtemps ma passion c’était quand même la programmation, les langages de programmation, comment expliquer ce que fait un programme, comment prouver qu’il est correct, comment trouver de la sémantique, comment programmer de façon élégante, comment avoir des abstractions des langages de programmation. C’était assez étonnant de voir comment dans le monde de la recherche l’activité de programmation était, d’une certaine façon, pas suffisamment respectée on pourrait dire. C’était souvent vu comme un outil par pas mal de disciplines. D’ailleurs, quand j’ai commencé mes études en Italie à Pise, à l’École normale, je pense que nous étions quatre informaticiens quand nous sommes entrés. Tous les autres nous regardaient un peu mal en disant « tu es informaticien, donc tu es un mauvais physicien avec une calculette ! », ou alors « tu es un mauvais mathématicien avec une calculette. »
Paul De Brem : Pour revenir à Software Heritage, justement à cette diapositive, donc on a 12 milliards de codes sources. On a des petites pépites. On a par exemple, à gauche, le code source de Apollo 11, c’est ça ? C’est le système informatique qui se trouvait à bord ?
Roberto Di Cosmo : À bord de Apollo 11 pour les systèmes de guidage. Ça permet d’ailleurs de faire un peu d’histoire. Au moment où le projet Apollo a été lancé, on calcule aujourd’hui que cet objet, cet énorme programme industriel, a coûté l’équivalent de 200 milliards de dollars actuels, il n’y avait pas une ligne budgétaire pour le logiciel.
Paul De Brem : Pas une ligne budgétaire.
Roberto Di Cosmo : Il n’y avait pas de ligne budgétaire pour les lignes de code, ce n’était pas prévu, c’est arrivé plus tard. C’est peut-être grâce à ça que finalement on a eu une des premières femmes dans l’histoire de l’informatique, Margaret Hamilton [5], qui a piloté l’équipe qui a développé ce code-là.
La raison pour laquelle on a accès à ce code-là – ça c’est un petit bout, ce n’est pas très visible, ce n’est pas très bien focalisé, mais je peux vous die ce qu’il y a dedans.
Paul De Brem : À droite je vois INITIALIZE LANDING RADAR.
Roberto Di Cosmo : À l’époque, aux États-Unis, tout ce qui était financé sur des fonds fédéraux était automatiquement mis dans le domaine public sauf s’il y avait des questions de sécurité. C’est pour ça qu’on a accès à tout ce code qui est dans le domaine public.
Vous voyez, à gauche, un truc qui ressemble à du charabia, c’est de l’assembleur de l’époque, et à droite les commentaires écrits en anglais de l’époque étaient un message envoyé par les développeurs aux autres développeurs. Comme disait Donald Knuth [6] dans une citation que je considère assez célèbre « finalement la programmation c’est l’art d’expliquer à un autre être humain ce qu’on souhaite qu’un ordinateur fasse ». Et c’est super important de l’expliquer bien, comme disait Harold Abelson [7] dans la citation que vous avez tout en haut dans ces transparents, parce qu’on a besoin de pouvoir le relire plus tard, de pouvoir le faire évoluer, de comprendre ce qu’il y a dedans. Pourquoi tout ceci est important ? En réalité, même si on a des algorithmes qui sont des descriptions de très haut niveau de comment on peut résoudre un problème, après, pour les faire exécuter par une machine, il faut décrire dans les détails ce que l’on veut dans un langage de programmation donné et dans ces détails il y a des fois énormément de connaissances supplémentaires qu’on ne retrouve ni dans les articles ni dans la description des algorithmes. Donc c’est absolument essentiel d’avoir accès à ces codes sources. Ceci est un pilier de ce mouvement de la science ouverte à laquelle on s’intéresse de plus en plus aujourd’hui qui est essentiel pour faire en sorte que nos concitoyens puissent avoir plus de confiance dans les résultats des recherches scientifiques, puissent vérifier ou demander à d’autres, si eux ne sont pas capables, de regarder ce qui a été fait pour valider que ces résultats scientifiques sont valables. C’est essentiel comme on a vu dans ce phénomène de covid parce que la perte de confiance dans la connaissance scientifique est la base de la perte de confiance dans le fonctionnement d’une société.
Paul De Brem : Pour revenir à Software Heritage, à droite on a aussi le code source de QUAKE III qui est un jeu vidéo, vous avez aussi le premier navigateur internet, le noyau Linux qu’on trouve à l’intérieur des smartphones Android, tout ça peut être utile pour faire de la recherche et comprendre comment tout çà été créé. Est-ce que vous avez l’impression, l’un et l’autre, que le logiciel a été un peu négligé par le passé et que, de plus en plus, on comprend sa valeur et on comprend l’importance d’avoir des programmateurs, des gens qui vont faire du logiciel libre, du logiciel de recherche pour toute la communauté ? Mihaela.
Mihaela Sighireanu : Oui, je pense qu’on a gagné justement cette expérience par le passé. Les idées de recherche fondamentale sont très bien on a besoin de ça, mais le prototypage de ces idées, le prototypage des algorithmes est aussi très important pour se confronter à d’autres algorithmes, pour voir aussi quelles sont les bonnes idées à prendre par ailleurs. On a vu justement apparaître, dans la plupart des conférences internationales, des sections où on incitait ceux qui avaient proposé de bonnes idées de recherche de soumettre aussi leurs artefacts qui étaient ensuite validés par un comité de programmes différent, indépendant. Oui, je pense qu’on se dirige vers une reconnaissance du logiciel aussi en tant que production scientifique et je pense que c’est très bien.
Roberto Di Cosmo : Je peux peut-être ajouter trois petits éléments là-dessus. Vous demandiez si on va vers une vraie reconnaissance. Déjà le fait de l’existence d’une infrastructure comme Software Heritage qu’on est en train de construire pour archiver tous les codes sources sur la planète, pas juste pour garder des codes poussiéreux pour des passionnés qui vont regarder les choses d’il y a 50 ans, mais aussi et surtout pour regarder comment le code est développé et pouvoir tracer aujourd’hui les vulnérabilités, les modifications et les évolutions. Le fait que cette initiative soit soutenue par des organismes comme l’Inria, le CNRS, Sorbonne Université et aussi Paris Cité, quel hasard, nous sommes tous ici, je prends cette occasion pour remercier à nouveau d’avoir eu confiance dans ce projet à un moment où c’était un petit bébé qui est en train de grandir maintenant.
Paul De Brem : L’Unesco aussi, vous avez le parrainage de l’Unesco.
Roberto Di Cosmo : Bien sûr, il y en a plein, je remercie d’abord ceux qui sont présents.
Je voulais aussi préciser parce que vous dites que je suis fondateur, président, c’est très égocentrique, je préfère dire que c’est un effort collectif. Il y a pas de mal de gens de l’équipe qui sont ici. On a travaillé avec Stefano [Zacchiroli], on a travaillé avec Jean-François [Abramatic], on a travaillé avec Nicolas [Dandrimont], on a travaillé avec Morane [Gruenpete], plein de gens qui sont ici et c’est vraiment important de reconnaître qu’il s’agit d’un effort collectif, comme disait un vieux proverbe africain Tout seul on va plus vite mais ensemble on va plus loin. On essaye de prendre ça systématiquement.
Deuxième élément de reconnaissance. Le fait que de plus en plus on retrouve le logiciel, comme disait Mihaela, justement comme un produit de la recherche, vraiment valorisé en tant que tel. Le fait que cette valorisation a lieu c’est par exemple que cette année, pour la première fois dans le monde, un ministère, le ministère de la Recherche français, a créé un prix national pour les logiciels de recherche [8] dans lequel on retrouve 129 candidatures d’excellente qualité et, parmi les lauréats, il y a des logiciels de cette université, de Sorbonne Université, mais aussi Paris-Cité, de l’Inria, du CNRS dans toutes les disciplines.
Le troisième élément que je voulais mentionner c’est le fait que finalement l’activité de programmation commence à être vue comme une activité noble et non plus seulement quelque chose qu’on peut outsourcer en Inde, en Tunisie, le near-shore comme on disait autrefois, etc. On a compris que finalement le pouvoir est dans les mains de ceux qui savent écrire le code qui devient la loi, comme disait Lawrence Lessig [9] Code is Law.
Si vous me permettez je termine juste avec une phrase. Il y a des choses révolutionnaires qu’on commence à faire. Par exemple, plus récemment, on a des projets qui nous montrent comment on peut faire l’inverse, transformer la loi en code, n’est-ce pas ! Faire en sorte que la loi devienne exécutable. Ça fait une peu peur, si on passe une mauvaise loi elle est exécutée tout de suite ! Par exemple sur le code fiscal, savoir comment nos impôts sont calculés, pouvoir vérifier comment c’est fait grâce à projet qui est basé sur des langages de programmation modernes avec toutes les notions des langages de programmation de base. On est en train de formaliser tout ça et ça va être utilisé au ministère de Finances.
Mihaela Sighireanu : Je voulais tout simplement ajouter, je ne l’ai pas dit tout à l’heure, le fait que toute la recherche fondamentale sur les langages de programmation est aussi quelque chose d’important, parce qu’on parle de logiciels. C’est important que nous, en tant qu’experts en informatique, on puisse exprimer, programmer dans des langages adaptés et la communauté des deux laboratoires a eu des contributions importantes dans ces langages de programmation, des langages de programmation fiables pour les systèmes, je pense au langage synchrone, au langage fonctionnel, au langage impératif. La recherche fondamentale nous permet justement de capturer cette spécificité des chercheurs, des non chercheurs aussi, pour pouvoir programmer mieux, de manière plus fiable, de pouvoir exprimer nos algorithmes dans des langages adaptés.
Paul De Brem : Le ministère de la Recherche a créé les Prix science ouverte du logiciel libre et de la recherche, il y a plusieurs prix, c’était cette année et c’est vraiment le signe que quelque chose est en train de se passer de côté-là et que de plus en plus les créateurs de logiciels sont reconnus, y compris dans l’évaluation de leur carrière, je crois qu’il en est question de plus en plus.
Merci infiniment à tous les deux d’avoir été avec nous.
[Applaudissements]