Décès de Robin Milner

L’informatique théorique est une science jeune : bien que certaines de ses idées (dont l’algorithme d'Euclide) remontent à plusieurs millénaires, la plupart de ses grands noms sont encore en vie, et même souvent encore en activité aujourd’hui. La mort de Robin Milner, le 20 mars dernier, à l’âge de 76 ans, nous rappelle que c’est une chance rare, mais aussi une époque qui touche à sa fin.

Né dans une famille de la classe moyenne anglaise, ses résultats scolaires ont permis au jeune Robin Milner d’accéder à une éducation privilégiée, en gagnant des bourses pour l’Eton college en 1946 puis pour l’université de Cambridge en 1952. Il y développa une passion pour les mathématiques et la musique (il jouait du hautbois).

Après avoir envisagé de devenir musicien professionnel, il devint professeur de mathématiques en 1957, puis programmeur chez Ferranti (une firme anglaise qui a développé certains des tous premiers ordinateurs). En 1968, il partit aux États-Unis pour faire de la recherche dans deux domaines balbutiants : l’intelligence artificielle et la preuve assistée par ordinateur. C’est là qu’il développa la première version du système LCF (en), un logiciel que je décrirai rapidement dans la deuxième partie de cette news.

En 1973, Milner rentra au Royaume-Uni avec sa femme, professeur de violon, pour travailler à l’université d’Édimbourg. Il continua le développement du système LCF, pour lequel il développa un nouveau langage de programmation, ML, qui influence toujours de nombreux aspects des langages de programmation modernes.

À partir des années 80, Milner consacre la majorité de son temps de recherche à un sujet qui l’a toujours intéressé, la concurrence : comment modéliser une interaction entre plusieurs systèmes qui fonctionnent simultanément et qui communiquent entre eux ? Il développa le système CCS (en) (Calculus for Communicating Systems), puis le Pi-calcul, langage aujourd’hui à la base des études théoriques des systèmes concurrents.

En 1991, Milner gagna le Turing Award, une des plus prestigieuses récompenses en informatique. Il continua à faire de la recherche jusqu’à sa mort : il passa un an à travailler en France en 2007, et publia en 2009 un livre sur les bigraphes, ses travaux les plus récents dans le domaine de la concurrence.

Robin Milner a marqué les esprits par son insistance sur l’élégance et la rigueur mathématique, les liens entre les aspects théoriques et pratiques des langages de programmation, ses qualités d’administrateur, d’enseignant et de chercheur. Il a toujours fondé sa recherche sur des problèmes pratiques auxquels il apportait des solutions puissantes et flexibles, grâce à l’élégance et au minimalisme des concepts mathématiques de la théorie.





Sources :

• Rubriques nécrologiques : Cambridge University (en), Times (en), The Guardian (en), LinuxFR (fr)
• Article Robin Milner sur wikipédia (en)
• An interview with Robin Milner (en) : une très longue interview (en anglais) de Robin Milner. Elle date de 2003 et a été menée par Martin Berger, lui-même chercheur en informatique, donc est parfois très approfondie.
• A Brief Scientific Biography of Robin Milner (en)

LCF

Milner s’était initialement intéressé aux bases de données : comment répondre automatiquement à une requête de l’utilisateur ? Il a ensuite travaillé sur des prouveurs automatiques, qui répondent à d’autres formes de requête : cet énoncé mathématique est-il valide ? Par exemple on lui demande : "Est-ce bien vrai que pour tout nombre entier , le nombre est pair ?", et il répond : Oui.

C’est un domaine très intéressant, qui est encore un sujet de recherche aujourd’hui, mais qui est toujours fortement limité : trouver des preuves d’énoncés mathématiques intéressants est une activité très difficile, que les ordinateurs ont beaucoup de mal à effectuer automatiquement. L’étape suivante, si l’on veut faire des mathématiques avec un ordinateur, est de passer à un modèle hybride où l’humain peut aider la machine : c’est le principe des assistants de preuve. L’humain donne des indications à l’ordinateur sur la façon dont il faut faire la démonstration mathématique, et le programme se charge de vérifier qu’il n’y a pas d’erreur, que toutes les étapes du raisonnement sont valides.

C’est ce que faisait LCF, un des premiers logiciels de ce genre. Les preuves sont décrites au logiciel sous des formes très strictes, pour qu’il puisse les comprendre. Dans la première version LCF, seul un petit nombre de règles de déduction (« pour prouver ça, il suffit de prouver ceci et cela ») étaient disponibles, mais le système a rapidement été rendu extensible, grâce un langage de programmation dédié que je présenterai dans la section suivante.

Ces outils ne sont pas utiles qu’en mathématiques, mais peuvent aussi servir dans tous les domaines scientifiques, donc en particulier en informatique. À l’époque (début des années 1970), l’informatique théorique avait été mise en ébullition par les travaux de Dana Scott, qui ont permis d’étudier mathématiquement la signification (sémantique) des programmes informatiques. Milner a ainsi utilisé LCF pour vérifier un petit compilateur : si on sait exprimer mathématiquement le sens d’un langage de programmation, et aussi le sens du langage assembleur, on peut prouver qu’un compilateur est correct, c’est-à-dire que le programme assembleur qu’il produit est équivalent au programme dans le langage qu’on lui a donné. C’était à l’époque un essai sur un langage très simple, mais de nos jours on fait des preuves beaucoup plus ambitieuses, comme la vérification complète d’un compilateur du langage C.

Source : From LCF to HOL : a short history (en), par Mike Gordon, un des collaborateurs de Milner.

ML

Avoir un logiciel qui aide à faire des démonstrations, c’est très bien. Mais quand il tombe entre les mains d’une équipe d’informaticiens… ils ont vite envie de programmer ! On peut avoir envie, par exemple, d’écrire des programmes qui font automatiquement certaines parties de la preuve qui sont plus faciles. Cependant, si on laisse les utilisateurs étendre le logiciel avec des scripts, il se pose assez vite une question délicate : si le script utilisé est buggué, est-ce qu’on risque d’obtenir des preuves fausses ?

Il y a plusieurs façons d’éviter ce problème, mais la méthode utilisée par LCF fut totalement novatrice : utiliser le typage du langage de programmation des scripts pour empêcher les preuves erronées. On représente les théorèmes par un type abstrait de données (en), dont les seules opérations disponibles correspondent à un petit ensemble de règles de raisonnement valides. Toute manipulation incorrecte est rejetée comme une erreur de typage par le compilateur. Ainsi, un utilisateur peut écrire un script qui manipule les démonstrations comme il le souhaite, il est sûr qu’il n’introduira jamais d’erreur de raisonnement sans en être averti.

Pour pouvoir faire cela (donc répondre à un problème très concret), Milner a conçu un langage de programmation entièrement nouveau, nommé ML. Cela signifie « Méta-langage », un langage de programmation qui manipule le langage des preuves. Milner et les gens qui travaillaient avec lui se sont peu à peu rendu compte qu’il pouvait en fait servir de langage de programmation généraliste, qu’on pourrait utiliser dans beaucoup d’autres contextes. Ce fut le début des langages de programmation « de la famille ML », comme OCaml, Standard ML (en), et aussi Haskell, qui ont repris le système de typage novateur.

Source : A theory of type polymorphism in programming (en), l’article original de Milner sur le système de typage du langage ML.

Fonctionnalités novatrices du typage ML

Le premier atout du système de typage de ML est le polymorphisme paramétrique. C’est une façon d’exprimer la généricité d’une fonction dans son type : il indique qu’elle peut en fait s’utiliser avec de nombreux types différents, de la même manière à chaque fois. Pour cela, on écrit des « variables de type » ('a, 'b, …), que l’on peut remplacer ensuite par n’importe quel type. Par exemple, la fonction qui renvoie la taille d’une liste est de type 'a list -> int, donc on peut l’utiliser sur des listes d’entiers (int list), de chaînes de caractères (string list), de fonctions entières ((int -> int) list)… La fonction qui prend une liste et renverse l’ordre des éléments est de type 'a list -> 'a list : elle prend une liste de n’importe quel type, et renvoie une liste du même type.

Cette idée était déjà connue des mathématiciens (logiciens), mais n’avait encore jamais été mise en pratique dans un langage de programmation. De nos jours, elle est la base de plusieurs d’entre eux, ainsi que des generics de C# ou Java.

La seconde caractéristique du typage ML est l’inférence de types : en ML, il n’est jamais nécessaire de préciser le type d’une variable, le compilateur le devine tout seul. On reproche souvent aux langages statiquement typés leur verbosité, liée en particulier à la déclaration du type de chaque variable. ML allie la rigueur et la sûreté des langages statiques, avec une certaine légèreté des langages dynamiques. De plus, comme tout ce qui a été conçu par Milner, la rigueur est au rendez-vous : il n’y a jamais de bricolage et le type deviné est toujours le type le plus général possible. Cette inférence est restée longtemps un trésor réservé à des langages fonctionnels peu connus, mais commence enfin à apparaître dans les langages de programmations « grand public » , avec par exemple Scala et C#.

Concurrence et Pi-calcul

Un autre domaine qui a toujours intéressé Milner est la question des interactions entre différents systèmes. Comment représenter et étudier la communication entre différents ordinateurs ?

Il se consacre pleinement à la question à la fin des années 70. C’est une question pratique très pertinente à l’époque : les réseaux entre ordinateurs commençaient à se répandre : le protocole TCP avait été publié en 1974, mais le premier déploiement de réseau d’envergure sous TCP/IP date de 1983. Mais Milner a une vision qui dépasse un cadre donné : il veut un système théorique qui décrit l’interaction entre systèmes et qui soit applicable dans un cadre très large : programmes au sein d’un ordinateur, réseau d’ordinateurs, protocoles de communication, échanges entre des personnes humaines, etc.

En 1980, il publie un livre intitulé A Calculus of Communicating Systems, qui présente sa première réalisation de poids dans le domaine. C’est un langage théorique du même nom (CCS), dans lequel on peut modéliser des systèmes qui évoluent indépendamment, mais qui se synchronisent sur certaines actions.

Par exemple, si vous allez acheter du pain à la boulangerie, vos actions sont indépendantes de celle de votre boulanger, mais il y a un cas particulier de synchronisation : quand vous lui tendez de l’argent, il vous donne du pain, et inversement; l’un n’arrive jamais sans l’autre.

Les applications de ce système CCS sont vastes, de la modélisation d’un distributeur de boissons à l’étude fine de protocoles de communication : est-il possible, par exemple, que deux systèmes se bloquent mutuellement, chacun attendant de l’autre une synchronisation qui ne vient pas ?

Cependant, CCS a des limitations : il ne permet pas de modéliser des réseaux dans lesquels des liens entre deux systèmes se créent ou disparaissent, où la structure du réseau évolue au cours du temps. Milner connaissait ce problème et avait essayé d’intégrer cet aspect à CCS, mais cela n’avait pas marché. Au cours des années 1980, les travaux d’autres chercheurs ouvrent la voie à un modèle plus flexible, et Milner (avec deux autres chercheurs nommés Joachim Parrow et David Walker) les étudie et les améliore entre 86 et 89 : il obtient Pi-calcul (comme la lettre grecque π, choisie un peu au hasard).

C’est un nouveau langage théorique dans lequel les canaux de communications eux-mêmes peuvent être échangés entre les différents systèmes : si j’ai un lien de communication avec A, je peux l’envoyer à B, qui pourra lui aussi parler à A. Ainsi, le réseau peut se reconfigurer au fil du temps. Autrement dit, dans le Pi-calcul, les liens de communication sont eux-mêmes mobiles.





Avec ce formalisme, on peut modéliser la plupart des processus concurrents que l’on rencontre en informatique. L’intérêt d’avoir un modèle théorique, c’est qu’il permet de réduire des systèmes réels, très très compliqués, vers une forme plus abstraite et plus simple, dont on peut étudier les propriétés fondamentales. Par exemple, il est difficile aujourd’hui d’écrire des programmes concurrents (où plusieurs parties du programme s’exécutent indépendamment et interagissent), et cela peut donner lieu à des erreurs très difficiles à repérer, et à corriger. Plutôt qu’essayer de raisonner sur le code concret du programme, qui est très long et très compliqué, le programmeur peut s’arrêter un instant, prendre un papier et un crayon, et construire un modèle du programme (par exemple dans le pi-calcul), qui lui permette de vérifier que la conception ne contient pas d’erreur (pas de risque de blocage du système, d’erreur de synchronisation, etc.) : le système théorique lui donne des outils pour vérifier tout cela rigoureusement. Une fois qu’il est sûr que la conception du programme tient la route, il peut se concentrer sur l’implémentation, qui recèle ses propres difficultés.

Le Pi-calcul a ainsi été utilisé dans des situations très variées : en informatique, il permet de modéliser l’exécution des programmes concurrents, mais aussi par exemple des aspects de sécurité de l’information : est-ce que les données importantes risquent d’être envoyées sur le réseau ? En dehors de l’informatique, il a aussi été adapté pour représenter des réactions chimiques et des systèmes biologiques : un système moléculaire peut être très complexe (énormes molécules, réactions impliquant de nombreuses molécules..), et le Pi-calcul permet de représenter les interactions qui s’y déroulent.

Mais tout n’est pas encore joué : la recherche de modèle d’interactions concurrentes est encore un sujet de recherche actif. De même que Milner était bien conscient des limitations de CCS, certains chercheurs discutent de modifications du Pi-calcul, ou de systèmes alternatifs, et la recherche du langage théorique ultime continue. Milner lui-même y participait, avec son travail sur les bigraphes à la fin des années 2000.

Sources :

• Communicating and mobile systems : the π-calculus (en) : livre introductif de Robin Milner.
• A Calculus of Communicating Systems with Label Passing - Ten Years After (en) : article de Engberg et Nielsen racontant leur rôle dans le passage de CCS au π-calcul.

Quelques citations pour finir

Pour récompenser le courage de ceux qui ont lu la news jusqu’ici, voici quelques citations de Robin Milner.

Robin Milner raconte sa première rencontre d’un ordinateur, en 1956 : à l’époque, il est choqué par le manque d’élégance des langages de programmation utilisés.

Citation



Citation