Ce point d'étape tombe à pic, au moment où, malgré les rivalités électoralistes régionales entre M. Blanc et Mme Pécresse, un consensus sur l'aménagement du plateau de Saclay, au sud de Paris, en un grand centre de recherche et d'éducation scientifique se dégage finalement. En mai 2008, Nicolas Sarkozy n'avait-il pas déclaré vouloir « une véritable Silicon Valley sur le plateau de Saclay » ? Le clou était d'ailleurs enfoncé, s'il en était encore besoin, par Pierre Lasbordes, député de la 5e circonscription de l'Essonne, qui martelait, en conclusion de la journée, toutes les initiatives régionales issues de la volonté publique : L'Agence nationale de la recherche, les labels Carnot, le pôle de compétitivité — le plus important des « pôles à vocation mondiale », excusez l'emphase ! —, le Crédit impôt recherche, l'Association Bernard Gregory, etc. Avec tout ça, nous disait-il en substance, étonnez vous que le « privé soit en retard sur Lisbonne » ! (Ce qui, aimablement traduit du vernaculaire européano-commissionnaire par mon voisin, apparemment fonctionnaire de longue date au fait de l'onomastique bruxello-administrative, signifierait, sur une tonalité menaçante, que l'investissement en recherche du secteur privé fait pâle figure devant la manne somptuaire complaisamment déversée par la puissance publique, ce en contradiction flagrante des objectifs stratosphériques de la stratégie de Lisbonne adoptée, en grande pompe par l'Europe en 2000, dans l'œil du cyclone de la Bulle Internet — visées maintenant communément jugées au mieux délirantes par la grande majorité des observateurs.) À ce titre, concluait l'élu, le partenariat public-privé entre MSR et l'Inria était « exemplaire ».
C'était également l'avis de Michel Cosnard, président directeur général de l'Inria, et celui d'Eric Boustouller, président de Microsoft France venus témoigner de l'union des forces vives de recherche de l'excellence informatique française et de la bienveillance industrielle du géant de l'informatique. Ceci dit, il ne nous a pas été donné de savoir si ce partenariat, à l'origine d'une durée de trois ans et venant, par conséquent, à échéance à la fin de l'année serait effectivement renouvelé. Excellence de la recherche française, certes, mais sous observation de nos estimés collègues britanniques issus de l'Université de Cambridge au Royaume-Uni, où est installé l'un des cinq laboratoires de MSR dans le monde, et sous qui est formellement placée la responsabilité du Centre commun de recherche.
C'est aussi en pleine campagne KES que les chercheurs venaient présenter leurs travaux et leurs résultats dans l'amphi Pierre Faurre. (Et c'est heureux : la journée de carnaval décrétée par la promotion permettant aisément au novice de distinguer d'emblée les élèves, costumés et bariolés, des chercheurs, enfermés depuis deux ans avec leurs abstractions mathématico-informatiques dans la ferme du Moulon, exfiltrés en goguette pour quelques heures !) Deux grands axes de recherche ont été mis en place à la création du laboratoire :
· Spécification, programmation et preuves formelles ;
· e-Science
en fait, deux domaines qui recouvrent essentiellement les travaux des équipes de l'Inria qui rejoignirent le Joint Research Centre il y a deux ans.
En guise d'introduction, Georges Gonthier, rappelait qu'au coeur de ces recherches gisait une polémique ancienne sur le rôle de l'ordinateur en mathématiques.
Sur son propre sujet de recherche, la résolution du problème séculaire des quatre couleurs par Appel et Haken en 1976, à l'aide d'un calcul compliqué sur ordinateur, fût le début d'une polémique sur l'utilisation des ordinateurs en mathématiques : un tel calcul pouvait-il vraiment avoir valeur de preuve ? Trente ans plus tard, Georges Gonthier pouvait enfin répondre par l'affirmative : il est possible de construire effectivement une preuve complètement formelle du théorème des quatre couleurs.
Et donc l'ordinateur peut, en effet, jouer un rôle essentiel en mathématiques et dans l'avancement du progrès informatique : les programmes peuvent prouver les calculs (mathématiques), ils peuvent faciliter la relecture et la revue des études mathématiques — on pense ici aux nombreux rebondissements dans la vérification par la communauté des mathématiciens de la preuve du théorème de Fermat par Andrew Wiles entre 1993 et 1994 —, et enfin, les ordinateurs permettent d'explorer les structures mathématiques.
Ces rôles importants étaient tour à tour illustrés par le travail du Centre commun de recherche sur les « composants mathématiques » réutilisables dans les preuves formelles, une forme curieuse d'application des concepts de la programmation orientée-objet à l'élaboration de preuves mathématiques. Dans cet esprit, une preuve est analogue à un programme informatique et le système mis au point ici, la preuve est un « script » compilé en preuves Coq qui peuvent être vérifiées automatiquement. Georges Gonthier démontrait l'application de ses idées à l'imposant théorème de Feit-Thompson, mais des applications techniques plus pratiques étaient présentées par les orateurs suivants, en particulier à la certification des calculs parallèles et d'algorithmes cryptographiques. (Malheureusement bien plus des sujets d'actualité aujourd'hui que la classification des groupes finis pourrait-on déplorer.)
Microsoft envisage même — défense de ricaner — de certifier le code des fameux device drivers de Windows grâce à ces méthodes formelles. On leur souhaite beaucoup de courage !
Au passage on apprenait que le langage de programmation privilégié pour développer les applications pratiques des preuves formelles chez MSR est F# avec, en particulier : F7 pour la vérification des types, et Z3, un theorem prover, c'est-à-dire un automate de preuve formelle.
Autre front, autre progrès : les spécifications formelles. Depuis que Leslie Lamport avait rejoint MSR, on savait leurs laboratoires fervents prosélytes de TLA+. (Leslie Lamport est universellement connu — en informatique scientifique tout du moins — pour avoir développé LaTeX, sur la base du célèbrissime TeX de Donald Knuth.) Leslie Lamport a également mis au point Paxos, un algorithme de calcul distribué pour la tolérance de pannes. (Paxos est utilisé par Google pour son maintenant fameux Google File System, par exemple). Les travaux de son groupe, présentés à l'occasion de cette journée, visent à étendre TLA+ avec un système de preuve formelle automatisé. Réutilisant des travaux antérieurs de l'Institut français, ces extensions de la spécification aux preuves sont traduites en Isabelle qui certifie les preuves générées par Zenon, l'automate de preuve formelle de l'Inria.
Il est à noter que les chercheurs de MSR rattachés à ce premier axe de recherche informatique ont progressivement envahi toutes les conférences internationales techniques sur le sujet, en particulier la série annuelle des conférences Principles of Programming Languages, affectueusement nommées POPL par les familiers. Tous ces articles et papiers sont publiés et le code et les exemples utilisés sont en général libres d'accès, signe de la vivacité de la recherche à Microsoft et de son ouverture la plus large à la communauté de la recherche en informatique.
Le second axe de recherche du Centre commun de recherche MSR/Inria a trait à l'e-Science, c'est-à-dire dans la plus grande généralité aux usages de l'informatique pour assister les scientifiques dans leurs travaux de recherche. Réflexion spéculaire sur le travail et les pratiques des chercheurs, elle s'inspire des sciences cognitives, de l'esprit des encyclopédistes et de la modélisation des algorithmes.
Bruno Salvy, que nous avions déjà croisé à l'occasion de la visite extraordinaire de Donald Knuth à l'Ecole normale supérieure pour l'anniversaire de Philippe Flajolet, rendait à sa façon un hommage à deux héros de la protohistoire de l'informatique. Milton Abramowitz (1915-1958) and Irene Stegun (1919-) auteurs si méconnus d'une encyclopédie indispensable sont les discrets soutiers dont les efforts titanesques de recension et de compilation laborieusement égrenés au long des années, et que nul aède n'a encore chanté, ont permis l'élaboration de toutes les bibliothèques de calcul scientifique depuis les années soixante. Ce sont véritablement là les précurseurs de tous les programmeurs scientifiques des générations qui les ont suivis : telles celles des antiques computistes, qui supputaient les temps relatifs au calendrier ecclésiastique (cf. le dictionnaire de la langue française d'Emile Littré), les vies érémitiques d'Abramowitz et de Stegun furent, en leur temps, consacrées au comput des formules, expansions, intégrales, différentielles, rayons de convergences, approximations, tables et listes de toutes les fonctions essentielles de l'analyse mathématique.
Les travaux du Centre commun visent aujourd'hui à établir une version moderne de l'ancienne compilation, le Dictionnaire dynamique des fonctions mathématiques, qui serait automatiquement engendrée par programme et mise à la disposition de la communauté à des fins d'exploration de l'univers des équations algébriques et différentielles dans son ensemble.
Parmi les autres travaux présentés, ceux de Wendy Mackay autour d'un carnet de laboratoire interactif pour les travaux scientifiques, Reactivity — d'autant plus intéressant, qu'à quelque pas de là, la Bibliothèque de l'Ecole polytechnique exposait avec fierté certains de ses incunables, dont l'émouvant carnet de laboratoire de Henri Becquerel (1852-1908), Prix Nobel de physique en 1906. Mêlant remarquablement approche comportementale et visualisation de données (regardez ScatterDice et NodeTrix, par exemple), l'outil devient une mémoire interactive des notes et travaux de recherche du scientifique, ouverte directement sur le Web.
Les travaux de Marc Schoenauer, de l'équipe TAO de l'Inria, visent quant à eux à créer un « assistant de laboratoire » automatique : il s'agit d'utiliser des algorithmes de recherche combinatoire pour poser et résoudre des problèmes scientifiques. Enfin Jean Ponce, spécialiste de la vision artificielle, présentait d'impressionnant travaux liés à l'analyse d'images et de vidéos : reconnaissance au vol non seulement des formes, mais également des visages et des actions — fascinantes démonstrations sur des épisodes de la série Buffy contre les vampires ou des extrait du film Le Lauréat.
On le voit, au-delà de la satisfaction convenue sur l'excellent déroulement de la collaboration entre le géant de Redmond et l'échelon supérieur de la recherche française en informatique et en mathématiques, les résultats sont nombreux, ouvertement publiés et commentés par la communauté, rendus publics le plus largement possible et très innovants. De quoi prendre de court les critiques acerbes des débuts de cette collaboration, qui s'interrogeaient sur le montant versé par Microsoft pour mettre la main sur les résultats de labos de recherche financés par le secteur public ?
