dimanche, septembre 30, 2012

La Charge de la preuve

Largement passés inaperçus, tant les médias entretiennent une distance avec les mathématiques considérées comme rebutant les audiences populaires, les décès récents, à quelques mois d'intervalles, des grands mathématiciens Nicolaas Govert de Bruijn (1918-2012) et William Thurston (1946-2012) auraient du percer le voile épais dont il est conforme d'étouffer l'esprit réputé pusillanime du grand public. (À ce sujet, il serait innovant et probablement salutaire d'essayer de renverser la tendance à l'abrutissement des masses en diffusant quotidiennement la lecture d'un chapitre du Théorème vivant du médaillé Fields Cédric Villani avant le tunnel publicitaire de 20h40 !) Si les travaux théoriques de De Bruijn et Thurston en analyse et combinatoire (#) et en topologie et géométrie (#), respectivement, ne sont guère accessibles aux lecteurs régulier de I Can Haz Cheezburger, ils ont néanmoins donné lieu à des applications très concrètes et devenues fondamentales en informatique.

 

Ces éminents mathématiciens ont notamment tous deux mené une réflexion sur la notion de preuve en mathématiques (#) et sur sa relation avec celle de vérification d'un programme informatique. À une époque où l'ubiquité des logiciels et des équipements informatiques affleure dans les moindres échanges en société, celle-ci transforme et redéfinit la notion même de risque. Comme le prévoyait déjà le sociologue Ulrich Beck dans Risikogesellschaft, le risque intermédié par l'envahissant système technique est devenu invisible : nos cinq sens ne sont plus d'aucun secours pour nous guider quant à l'innocuité de notre alimentation bio ou OGM, quant aux dangers réels d'une politique industrielle du nucléaire aussi bien que de l'exposition de données privées sur le Net ou de la sécurité de nos transactions bancaires même les plus communes. Dans les secteurs de l'informatique triomphante, la mutation silencieuse du risque et la dépendance croissante de la société à aux technologies d'automatisation fut largement illustrée par le psychodrame à épisodes du « Bug de l'an 2000 ». Il apparut, dans ce cas, que toutes ces inquiétudes, soigneusement entretenues dans les dernières années du XXe siècle, n'étaient heureusement pas justifiées. En revanche, elles illustrèrent précisément la difficulté de « l'honnête homme » à formuler un jugement sur la nature et la qualité des risque encourus. En conséquence, le citoyen, l'usager, l'utilisateur quelque soit le rôle qu'il joue, est de plus en plus réduit à s'en remettre aux jugements d'experts, dont l'autorité, bien que représentant le dernier recours face à l'incommensurabilité commune du risque moderne, est de plus en plus critiquée publiquement tant s'amenuise corrélativement la confiance dans les progrès scientifiques et la « moralité » des milieux techniques. Alors — par défaut, ou par dépit ? —, l'impression que l'abondance de données, la confiance dans les nombres et le nombre, pourrait nous sortir de ce dilemme conduisit ces mathématiciens et d'autres grands pionniers de l'informatique à s'intéresser à la question de la preuve des programmes. Si l'on pouvait mathématiquement prouver un logiciel, cette vérification permettrait de quantifier explicitement le risque dans son usage et de mitiger l'épineux problème de la confiance dans le système.

 

Notons que cette vision irénique du quantitatif comme arbitre bienveillant rapiécant le tissu effrangé de la confiance entre acteurs humains des systèmes techniques est aujourd'hui sensible dans le mouvement Big Data, dans lequel, à l'extrême, rien moins que la vérité d'un business ou de l'action d'un gouvernement émerge de la volumétrie statistique des données — plus grand le datacenter, plus gros le volume de données et plus vraie la parole oraculaire du Big Data (Big Daddy ? #). Naguère, aux origines (militaires) des ordinateurs à programmes stockés, l'instant de réalisation cathartique de la crise du logiciel survint sans nul doute à la conférence de Garmisch-Partenkirchen en 1968 — où il n'est pas inutile, sinon patriotique, de rappeller le rôle important joué par le professeur Louis Bolliet (#) — , sur le software engineering, un néologisme qui devait déclencher d'âpres polémiques. Devant la complexité déjà atteinte par les systèmes techniques déployés à l'époque dans les banques, les télécommunications, ou la défense, il fallait s'armer d'outils et d'instruments d'analyse et d'ingénierie si l'on voulait déminer ce qui était déjà perçu comme une crise de confiance. Il en sortit la programmation structurée dont les champions Edger Dijkstra (1930-2002) et Harlan Mills (1919-1996) devaient s'affronter avec acrimonie quelques années plus tard sur l'impact social du software engineering au sein des organisations.

 

Les méthodes de test et de revue de code développés dans les années 1970 (#) renvoyaient explicitement la question de la fiabilité des logiciels à celle de la fiabilité des « experts » chargés de les appliquer. D'autres, parmi lesquels De Bruijn, cherchèrent à mettre en oeuvre des méthode déductives, issues de la logique mathématique, pour vérifier les programmes. Contemporains du développement, principalement européen — comme alternative à l'américain FORTRAN ? —, du langage de programmation ALGOL (#), les premiers appels à une formalisation mathématique de la vérification des programmes furent entendus dans les années 1960. Largement amplifiés par l'activisme de John McCarthy (1927-2011) disparu il y a presqu'un an, l'idée que l'informatique devait prendre comme modèle la physique mathématique fit son trajet dans les esprits de la communauté. L'un des premiers programmes écrits par McCarthy en LISP, le langage de programmation fonctionnel directement inspiré de la logique mathématique qui l'a rendu au moins aussi célèbre que ses travaux au MIT sur le timesharing — et dont un des gardiens du temple, Dan Weinreb (1959-2012 #), co-initiateur de la norme Common Lisp vient également de disparaître il y a quelques semaines — était un vérificateur de preuves.

 

Dans le même temps, et dans le mouvement inverse, De Bruijn démontrait l'intérêt de l'ordinateur dans le travail du mathématicien et, en particulier, dans la question duale de celle posée par McCarthy : de la vérification automatisée de la preuve mathématique. Son système, Automath (#) 1967-1975, reste le précurseur de la lignée des « assistants de preuves » qui avec NuPRL (#) et Coq (#), par exemple, sont devenus d'usage presque courant (#). Coq dont il n'est pas inutile, sinon patriotique, de rappeller que l'histoire a démarré en 1984 avec Thierry Coquand et Gérad Huet.

 

On à peine à imaginer aujourd'hui, à l'époque où le proof-carrying code (#) fait partie des mondanités échangées par les Microsoft dans tous les salons où s'élaborent les doctrines sociales du développement de logiciels, le caractère révolutionnaire des propositions d'un McCarthy et d'un De Bruijn. Tous deux furent l'objet de critiques nourries tant des mathématiciens que des hommes de l'art de la programmation et de l'informatique, à l'exception que quelques rares visionnaires comme Donald Knuth qui professe toujours une grande admiration pour De Bruijn et McCarthy (#). John Markoff raconte que Knuth se glissait régulièrement tous les soirs pour des séances de programmation nocturnes dans les laboratoires du Stanford AI Lab (SAIL #) créé par John McCarthy, arrivé du MIT à Stanford en 1962. Des dizaines d'années plus tard, des 1.700 utilisateurs du monumental PDP, c'était lui qui avait laissé le plus de fichiers.

 

Plusieurs grands pionniers attachèrent leurs noms à cet effort de formalisation logico-mathématique de la preuve de programmes : Peter Naur, Robert Floyd (1936-2001), Sir Charles Antony Richard Hoare parmi les plus connus. Du côté de l'instrumentation des mathématiques par les ordinateurs et les programmes, en revanche, les débats furent plus houleux dans les années 1960 et 1970. Après la conférence fondatrice de l'Intelligence Artificielle à Dartmouth en 1956, et la présentation par Allen Newell (1927-1992) et Herbert Simon (1916-2001) de leur Logic Theory Machine, un « prouveur de théorème », deux camps s'affrontèrent. Ceux qui, comme McCarthy et son ancien pair au MIT Marvin Minsky, imaginent doter la machine d'une intelligence différente de l'humaine, et ceux qui, comme Newell et Simon, s'attachent plutôt à l'explicitation de l'intelligence humaine par sa simulation (émulation ?) en machine. De même, en 1976, la démonstration assistée par ordinateur du fameux théorème des quatre couleurs par Appel et Haken (#) fut accueillie glacialement par la communauté des mathématiciens. Enfin les collègues de jadis, McCarty et Minsky, devaient s'affronter sur l'usage de la logique formelle pour représenter connaissances et raisonnements, le groupe de la côte Ouest devenu ardent zélateur du principe de résolution (#) du philosophe et mathématicien John Alan Robinson, point culminant de travaux entamés, sans vouloir remonter à Gerhard Gentzen (1909-1945), par les mathématiciens logiciens Dag Prawitz puis Hilary Putnam et Martin Davis, d'une part, et le groupe de la côte Est, avec Minsky et Seymour Papert qui en contestaient (bruyamment !) l'universalité, d'autre part. La contestation fut mise en sourdine en 1974 par un papier de Michael Fisher et Michael Rabin (#) sur « l'exponentialité du problème de la décidabilité de l'arithmétique de Presburger », une arithmétique simplifiée avec laquelle Martin Davis avait inauguré les contributions des mathématiciens logiciens à la question de la preuve des programmes. Il n'est pas inutile, sinon patriotique, de rappeler que de l'intérêt pour l'automatisation de la preuve des logiciels par la logique formelle, dérivait celui spéculaire pour la programmation logique, dans laquelle Alain Colmerauer s'illustrait avec Prolog qui séduisit le Japon le temps d'une génération (la cinquième).

 

Malgré les critiques contre la vérification formelle des programmes, renouvelée la décennie suivante par Alan Perlis (1922-1990), Richard Lipton, Richard DeMillo, puis par James Fetzer, le financement des recherches, notamment par les agences militaires américaines, sur ce sujet ne se tarissent pas au nom de la défense des intérêts nationaux. Nonobstant la différence établie entre les aspects « sociaux » de la pratique de la preuve et de sa vérification dans son avatar mathématique et la rigueur logico-déductive désirable pour son alter ego informatique — que l'on contraste le processus et la réception de la preuve d'Appel et Haken avec ceux de la preuve du théorème de Fermat par Andrew Wiles quinze ans plus tard — les méthodes formelles, malgré les théorèmes d'incomplétude de Kurt Gödel (1906-1978) — il n'est pas inutile, sinon patriotique, de rappeler aussi les travaux originaux de Jacques Herbrand (1908-1931) sur ce même sujet à la même époque — assurent aujourd'hui pour beaucoup le travail de Sisyphe d'allègement de la charge de la preuve.

 

ShareThis