Robin Milner a travaillé sur trois questions qui pourraient sembler séparées : comment faire vérifier une preuve par un ordinateur, comment laisser un compilateur déduire les types d’un programme et comment raisonner sur plusieurs processus qui communiquent. Il les a abordées avec une même exigence : construire des formalismes assez rigoureux pour établir des propriétés, mais assez maniables pour servir réellement aux informaticiens.
Cette démarche a produit LCF, une architecture fondatrice de la preuve assistée, puis ML, langage créé pour piloter ce système. Elle a également donné CCS et le pi-calcul, deux modèles majeurs de la concurrence et de l’interaction. Le prix Turing attribué à Milner en 1991 reconnaît précisément la portée de ces réalisations distinctes.
Son héritage ne tient donc pas à un unique langage. Il réside dans une manière de rapprocher théorie et pratique : la logique protège les garanties essentielles, tandis que le langage et les outils rendent ces garanties utilisables.
Des mathématiques à la programmation
Arthur John Robin Gorell Milner naît en 1934 à Yealmpton, dans le Devon britannique. Après des études de mathématiques à l’université de Cambridge, il travaille notamment chez Ferranti, l’une des entreprises pionnières de l’informatique commerciale au Royaume-Uni. Il enseigne ensuite et poursuit ses recherches dans plusieurs institutions avant de rejoindre Stanford au début des années 1970.
L’informatique de cette période doit apprendre à faire confiance à des programmes toujours plus complexes. Une démonstration mathématique peut décrire pourquoi un algorithme est correct, mais vérifier chaque étape à la main devient rapidement impraticable. À l’inverse, un programme de preuve très automatisé peut commettre un bogue et produire un résultat faux avec une apparence convaincante.
Milner cherche une troisième voie : laisser l’utilisateur et les programmes automatiser la construction d’une preuve, tout en forçant le résultat final à passer par un mécanisme de vérification réduit et contrôlable.
LCF : faire reposer la confiance sur un petit noyau
LCF signifie Logic for Computable Functions. La logique vient des travaux de Dana Scott sur les fonctions calculables ; Milner développe à Stanford en 1972 un premier système interactif permettant de construire des preuves dans cette logique. Le projet se poursuit ensuite à l’université d’Édimbourg avec Michael Gordon, Christopher Wadsworth et d’autres collaborateurs.
L’idée architecturale décisive consiste à représenter un théorème prouvé par une valeur d’un type abstrait. Le programmeur ne peut pas fabriquer librement une valeur de ce type. Seules quelques fonctions correspondant aux axiomes et aux règles d’inférence autorisées peuvent en produire une.
Cette séparation change le modèle de confiance. Les tactiques qui cherchent une preuve peuvent être nombreuses, sophistiquées et même contenir des erreurs. Si elles ne disposent d’aucun moyen de contourner le type abstrait des théorèmes, une erreur les empêche d’aboutir plutôt que de créer directement une fausse preuve. Le noyau logique, plus petit, concentre ce qui doit être inspecté avec la plus grande attention.
Les assistants de preuve HOL et Isabelle reprennent cette approche, souvent qualifiée d’architecture LCF. On la retrouve aujourd’hui dans la conception de nombreux outils où un noyau restreint valide les résultats produits par une couche d’automatisation plus large.
Pourquoi LCF avait besoin d’un nouveau langage
Un assistant interactif ne se contente pas d’appliquer une règle à la fois. Ses utilisateurs veulent écrire des stratégies : décomposer un objectif, simplifier une expression, essayer plusieurs règles puis combiner les sous-preuves obtenues. Le système doit donc être programmable.
Milner et l’équipe d’Édimbourg conçoivent un métalangage, bientôt abrégé en ML, pour exprimer ces stratégies. Le langage doit manipuler des arbres syntaxiques et des théorèmes sans confondre leurs formes, composer facilement des fonctions et empêcher qu’une tactique fabrique une preuve invalide.
ML privilégie pour cela les fonctions comme valeurs, les types algébriques, la reconnaissance de motifs, la récursion et une gestion automatique de la mémoire. Sa programmation fonctionnelle s’accorde naturellement avec la transformation d’expressions et la composition de tactiques.
Ce qui n’était au départ que le langage d’un outil de preuve se révèle suffisamment général pour devenir un langage de programmation à part entière.
L’inférence de types : obtenir des garanties sans tout annoter
Le typage statique peut détecter avant l’exécution qu’une opération reçoit une valeur incompatible. Mais si chaque variable et chaque fonction doivent porter de longues annotations, cette sécurité alourdit fortement l’écriture, en particulier dans un langage qui compose de nombreuses petites fonctions.
ML résout ce problème par une inférence de types polymorphe. Le compilateur analyse les contraintes créées par les opérations et déduit un type suffisamment général. Une fonction identité écrite sans annotation peut ainsi recevoir le type 'a -> 'a : quel que soit le type choisi pour 'a, elle reçoit une valeur et renvoie une valeur du même type.
L’algorithme couramment appelé Hindley–Milner doit son histoire à plusieurs travaux. Roger Hindley avait établi auparavant un résultat proche dans la logique combinatoire. Milner développe indépendamment un système de typage et un algorithme pratique pour ML, souvent désigné par la lettre W. Luis Damas en approfondit ensuite les propriétés avec lui, notamment la notion de type principal.
Un type principal représente la forme la plus générale compatible avec une expression. Les usages particuliers peuvent en être dérivés sans demander au programmeur de choisir prématurément un type concret. Ce compromis associe concision, réutilisation et détection statique d’une large classe d’erreurs.
L’inférence n’élimine pas tous les défauts. Elle garantit la cohérence des types selon le modèle du langage, pas la conformité d’un algorithme à son intention. Elle peut également produire des messages difficiles à interpréter lorsque la contrainte contradictoire se manifeste loin de son origine. Sa réussite vient néanmoins d’un équilibre rare entre puissance et prévisibilité.
Du ML d’Édimbourg à Standard ML
À mesure que ML est utilisé hors de LCF, plusieurs dialectes apparaissent. Une communauté réunissant chercheurs et implémenteurs entreprend dans les années 1980 de définir une base commune. Standard ML associe un langage fonctionnel strictement évalué à un système de modules élaboré.
Les structures regroupent des définitions ; les signatures décrivent les interfaces visibles ; les foncteurs construisent des modules à partir d’autres modules. Cette architecture permet de séparer l’implantation et le contrat à une échelle plus grande que celle d’une fonction.
Milner joue un rôle central dans la conception et surtout dans la définition formelle du langage, avec Mads Tofte, Robert Harper et d’autres collaborateurs. L’objectif n’est pas uniquement de publier un manuel informel. La sémantique doit préciser mathématiquement ce que signifie l’exécution correcte d’un programme et fournir un terrain solide aux implémentations.
Standard ML influence directement OCaml, tandis que les idées de la famille ML circulent dans Haskell, F#, Rust, Swift et de nombreux systèmes de types modernes. Ces langages ne reproduisent pas tous le même modèle, mais ils héritent de combinaisons devenues familières : types algébriques, motifs, polymorphisme paramétrique et inférence locale ou générale.
CCS : raisonner sur des programmes qui interagissent
Un programme séquentiel peut souvent être décrit comme une fonction qui transforme une entrée en sortie. Un système concurrent pose un autre problème : plusieurs composants progressent indépendamment, échangent des messages et réagissent à leur environnement. Son comportement dépend non seulement des calculs internes, mais aussi de l’ordre et de la possibilité des interactions.
Milner développe le Calculus of Communicating Systems, ou CCS, pour donner un langage mathématique à ces comportements. Un processus peut effectuer une action, choisir entre plusieurs évolutions, s’exécuter en parallèle avec un autre ou masquer certaines communications internes.
CCS rend possible une question essentielle : deux systèmes différents en apparence ont-ils le même comportement observable ? La bisimulation répond en comparant leurs transitions pas à pas. Si chaque action observable de l’un peut être reproduite par l’autre tout en conservant la relation, les deux processus peuvent être considérés comme équivalents selon le critère choisi.
Cette approche est compositionnelle. On peut étudier un composant, caractériser son comportement puis raisonner sur son insertion dans un système plus grand. Elle fournit des outils pour analyser des protocoles et des architectures concurrentes sans réduire l’interaction à une simple liste de résultats finaux.
Le pi-calcul : quand les connexions elles-mêmes se déplacent
CCS suppose essentiellement une structure de communication connue. Les réseaux et logiciels distribués introduisent cependant de la mobilité : un processus reçoit l’adresse d’un service, transmet un canal à un autre processus ou crée une connexion privée qui change ensuite de portée.
À la fin des années 1980 et au début des années 1990, Milner développe avec Joachim Parrow et David Walker le pi-calcul. Sa particularité est de permettre aux processus de communiquer des noms de canaux. Le réseau de connexions peut donc évoluer pendant le calcul.
Ce mécanisme compact peut représenter la création de sessions, le passage de capacités, la reconfiguration de services et diverses formes de mobilité. Le pi-calcul ne constitue pas une recette directe pour construire chaque système distribué. C’est un modèle volontairement réduit qui isole les notions de communication, de portée et de changement de topologie afin de pouvoir les étudier précisément.
Comme pour ML, la réussite vient de la relation entre un petit nombre de constructions et un vaste espace d’applications. Les travaux sont collectifs : Parrow et Walker participent à la formulation du calcul, tandis qu’une communauté entière en développe les variantes, les types et les outils.
Relier calcul, preuve et interaction
Milner rejoint l’université d’Édimbourg en 1973 et y reste plus de vingt ans. Il contribue à faire de la ville un centre majeur de recherche sur les fondements de l’informatique et devient le premier directeur du Laboratory for Foundations of Computer Science. En 1995, il rejoint le Computer Laboratory de Cambridge, qu’il dirige de 1996 à 1999.
Ses travaux ultérieurs cherchent encore à unifier les modèles de l’interaction. Les bigraphes représentent séparément la localisation des composants et leurs connexions, afin de décrire des systèmes mobiles ou omniprésents. Cette recherche prolonge le pi-calcul sans prétendre qu’un unique formalisme suffira à tous les logiciels.
Le fil conducteur est une science du calcul qui ne s’arrête pas au résultat d’une fonction. Une preuve est une construction contrôlée ; un type exprime une contrainte ; un processus est défini par ses interactions possibles. Dans chaque cas, le formalisme sert à composer de petits éléments tout en préservant une signification précise.
Pourquoi Robin Milner compte encore
Les langages modernes rendent souvent facultatives de nombreuses annotations tout en détectant les incohérences avant l’exécution. Les assistants de preuve combinent automatisation et noyaux de confiance. Les outils de vérification de protocoles comparent des états et des transitions. Ces pratiques appartiennent à des écosystèmes différents, mais les contributions de Milner ont aidé à établir leurs fondations.
Son parcours montre également qu’un langage spécialisé peut acquérir une portée générale. ML n’a pas été conçu à l’origine pour devenir une famille de langages applicatifs : il devait aider à écrire des tactiques de preuve. Les contraintes exigeantes de ce domaine ont produit des mécanismes utiles bien au-delà de LCF.
Enfin, Milner refuse l’opposition simple entre théorie et logiciel réel. Une théorie fructueuse doit expliquer ce que font les systèmes ; un outil durable doit reposer sur des idées que l’on peut formuler et discuter rigoureusement. C’est cette circulation entre modèles, langages et implantations qui rend son œuvre toujours actuelle.
Chronologie
- 1934 : naissance de Robin Milner à Yealmpton, dans le Devon.
- 1957 : diplôme de mathématiques à l’université de Cambridge.
- Années 1960 : travail dans l’industrie et l’enseignement, puis orientation vers la recherche informatique.
- 1972 : développement à Stanford du premier système LCF interactif.
- 1973 : arrivée à l’université d’Édimbourg.
- Années 1970 : développement d’Edinburgh LCF et création de ML avec ses collaborateurs.
- 1978 : publication de l’algorithme d’inférence de types associé à ML.
- 1980 : publication de l’ouvrage fondateur sur CCS.
- Années 1980 : conception et normalisation progressive de Standard ML.
- 1989–1992 : formulation du pi-calcul avec Joachim Parrow et David Walker.
- 1991 : attribution du prix Turing pour LCF, ML et CCS.
- 1995 : arrivée à l’université de Cambridge après vingt-deux ans à Édimbourg.
- 1996–1999 : direction du Computer Laboratory de Cambridge.
- 2010 : décès à Cambridge, à l’âge de 76 ans.
Questions fréquentes
Robin Milner a-t-il créé ML seul ?
Il en est le concepteur central dans le contexte de LCF, mais le langage et ses versions successives résultent d’un travail collectif à Édimbourg puis dans la communauté Standard ML. Michael Gordon, Christopher Wadsworth, Mads Tofte, Robert Harper et de nombreux autres chercheurs ont contribué aux systèmes, à la définition et aux implémentations.
Pourquoi ML a-t-il été créé ?
ML était d’abord le métalangage du système de preuve LCF. Il permettait d’écrire des tactiques qui construisent des preuves en combinant les règles sûres du noyau. Ses fonctions, ses types et ses motifs l’ont ensuite rendu utile comme langage général.
Qu’est-ce que l’inférence Hindley–Milner ?
C’est une méthode de typage qui déduit automatiquement un type polymorphe général pour de nombreuses expressions. Son nom reconnaît les travaux de Roger Hindley et de Robin Milner ; Luis Damas a ensuite approfondi avec Milner ses propriétés formelles.
Quelle différence existe entre CCS et le pi-calcul ?
CCS modélise des processus concurrents qui communiquent par des actions et des canaux. Le pi-calcul permet en plus de transmettre les noms de ces canaux : la structure des connexions peut alors changer pendant l’exécution.
Quel est le lien entre LCF et les assistants de preuve modernes ?
LCF a popularisé une architecture où seul un petit noyau peut créer les valeurs représentant des théorèmes. Des tactiques plus complexes recherchent les preuves, mais leurs résultats doivent être reconstruits à travers ce noyau. HOL et Isabelle descendent directement de cette approche, qui influence aussi d’autres systèmes de preuve.
