English Version
C'est le premier volume d'un travail monumental que Pierre Mounier-Kuhn consacre à l'histoire de l'informatique en France. Il traite de la recherche et l'enseignement supérieur ; le second volume traitera du comportement des constructeurs, le troisième du rôle de l'État.
Il faudra sans doute que Mounier-Kuhn consacre un quatrième volume à l'informatisation des institutions, à ce qui s'est passé du côté de l'utilisation, à ses exigences et ses relations avec les scientifiques, les fournisseurs et l'État.
Comme toute recherche en histoire, celle-ci est contrainte par la disponibilité des archives : elle s'arrête donc vers 1975. Or c'est à cette date que débute l'informatisation des institutions ainsi que celle de la société : la notion de système d'information émerge au début des années 70 et dès lors les exigences de la sémantique des données passent avant celles du calcul, qu'elles conditionnent en vertu du principe garbage in, garbage out.
Il s'agit de l'informatique en France, mais Mounier-Kuhn montre bien que notre pays, retardé par les circonstances de l'occupation allemande, n'a pas pu être un pionnier dans ce domaine. L'informatique a pris sa source aux États-Unis (et aussi en Grande-Bretagne), et les idées que nous autres Français avons pu avoir sur les compilateurs, systèmes d'exploitation, bases de données, réseaux etc. étaient de seconde main, réserve dûment faite pour quelques exceptions individuelles.
Il est donc difficile de décrire l'informatique en France sans remonter au réservoir d'idées et d'innovations américain d'où s'écoulait, chez nous, un filet relativement mince. Comment évoquer en effet les langages de programmation sans décrire leur naissance et celle de la compilation avec Fortran en 1954 (cf. L'émergence des langages de programmation) et les problèmes qu'a dû surmonter leur conception ? La même question se pose à propos des systèmes d'exploitation, bases de données, moniteurs transactionnels etc. Mais alors c'est une autre histoire qu'il faut écrire, située en amont de l'histoire de l'informatique en France qui, par comparaison, peut sembler minuscule : cette difficulté est inhérente au projet de Mounier-Kuhn.
Son livre montre bien l'ambiguïté des relations entre l'informatique et les mathématiques. À ses débuts l'informatique est un outil pour le calcul et se rattache donc aux mathématiques appliquées. Elle tente de conquérir une légitimité scientifique dans les institutions de recherche et les universités mais elle y rencontre le mépris envers les applications de la part des bourbakistes, ces obsédés de "pureté" qui ont fait des mathématiques un instrument de torture mentale.
Il est vrai que l'algorithmique pose de redoutables problèmes mathématiques : ceux que soulève par exemple le calcul en virgule flottante semblent même insurmontables [1]. Mais ici comme dans d'autres disciplines l'effort, d'ailleurs vain, pour se concilier les mathématiciens "purs" (ou du moins pour parer l'informatique du prestige des mathématiques "pures") a conduit à pousser la formalisation bien au delà de ce qu'exige l'algorithmique.
Une différence essentielle sépare en effet l'informatique des mathématiques : alors que celles-ci explorent un monde logique, donc indifférent à l'écoulement du temps comme à ses urgences, l'informatique est orientée vers l'action [2].
Il y a quelque chose de pathétique dans la tentative de la mathématiser : on souffre de voir cette discipline qui est orientée vers l'action, et qui est donc scientifique au sens exact du terme, singer laborieusement les mathématiques pour tenter de s'acquérir une réputation de scientificité. Cela la détourne de sa propre finalité, qui est essentiellement pratique, et cela ne fait d'ailleurs que renforcer l'hostilité qu'éprouvent envers elle les mathématiciens "purs".
Derrière ce conflit entre les mathématiques et l'informatique se pose la question, plus générale, des critères selon lesquels s'évalue la scientificité d'une discipline. Ceux qui croient que la science réside dans la rigueur des démonstrations oublient que celles-ci sont suspendues à des principes, des axiomes, que l'on ne démontre pas et qui délimitent ce dont on parle. Le réalisme des mathématiques est celui de la pensée soumise à la seule règle de non-contradiction. Le réalisme de l'informatique est celui de l'action, rencontre de la nature avec des intentions qu'orientent des valeurs.
Mounier-Kuhn décrit en détail les pénibles péripéties institutionnelles qui en résultent. À la lucidité exceptionnelle d'un François-Henri Raymond font pendant le carriérisme et la cuistrerie de plusieurs ainsi que des rêves fantastiques issus du fourre-tout de concepts-valise : cybernétique, intelligence artificielle, théorie des systèmes, logique floue, pensée complexe, voire même théorie de l'information.
Cette histoire est déjà ancienne et l'informatisation a transformé le paysage. Cependant les institutions mises en place avant 1975 sont toujours là et leurs priorités sont restées les mêmes : beaucoup d'étudiants en informatique n'entendent jamais parler des systèmes d'information (cette expression n'apparaît pas dans la formation des polytechniciens) ni de l'ingénierie sémantique qui leur sert de fondation. Ils auront dû ingurgiter équation sur équation et cela ne les prépare aucunement à comprendre ni l'informatique, ni moins encore l'informatisation.
____________________
[1] « Many serious mathematicians have attempted to analyze a sequence of floating point operations rigorously, but have found the task so formidable that they have tried to be content with plausibility arguments instead » (Donald Knuth, The Art of Computer programming, Addison-Wesley, 1998, vol. 2, p. 229)
[2] « In mathematics we are usually concerned with declarative (what is) descriptions, whereas in computer science we are usually concerned with imperative (how to) descriptions » (Harold Abelson et Gerald Jay Sussman, Structure and interpretation of computer programs, MIT Press 2001, p. 22).
Réflexion en marge de ce propos (que j'approuve naturellement ! en particulier sa conclusion) :
RépondreSupprimerJ'ai suivi à l'école des Ponts un cours superbe, magnifique, de "Logique et Informatique".
D'un point de vue d'informaticien, ça ne servait sans doute pas à grand chose. Les langages au formalisme le plus abstrait, genre CAML ou Prolog, sont restés marginaux pour autant que je sache.
Mais pour la mathématique, en l'occurrence pour la logique, ce n'était pas anecdotique. C'étaient de vrais beaux problèmes (et je n'en ai pas compris la moitié, à vrai dire). Du même tonneau que la topologie fondamentale ou que les processus aléatoires du second ordre (que je n'ai jamais compris du tout).
Alors c'est peut-être plus l'informatique qui a servi à faire progresser les mathématiques, que l'inverse ; et pourquoi pas ?...
Je n'ai pas lu le livre de Mounier-Kuhn (mais il est en attente sur ma table).
RépondreSupprimerTa position sur le sujet "informatique et mathématiques" (que j'approuve dans ses grandes lignes) appelle toutefois quelques nuances. Autant la formalisation pour la formalisation (à la Bourbaki, entre autres) est un exercice stérile, autant une "bonne" formalisation peut contribuer à des percées décisives. Je citerai deux exemples (il y en a bien d'autres).
- le "calcul des constructions inductives" développé depuis 20 ans à l'INRIA sur la base d'une nouvelle logique, la logique linéaire, permet aujourd'hui de prouver, au sens mathématique, qu'un programme est correct. Ces méthodes ont été appliquées pour prouver récemment la validité de programmes tels qu'un noyau de systèmes d'exploitation, un compilateur C, un système de gestion de bases de données. Le test (selon l'expression de Dijkstra) permet de montrer l'existence d'erreurs, non leur absence. Ici, il s'agit de tout autre chose : on PROUVE que le programme fait ce qu'on lui demande, et pas autre chose. Bien sûr, cela demande un travail considérable et la maîtrise d'outils très techniques ; et les programmes que l'on prouve sont encore des versions simplifiées. Mais la percée est maintenant effective. D'autre équipes dans le monde travaillent aussi sur ce sujet.
- Pour un objectif voisin, mais avec une approche très différente, l'interprétation abstraite permet de garantir, par une analyse du texte d'un programme, que l'exécution de ce programme sera exempte de certaines erreurs lors de l'exécution. Là aussi, les outils sont d'un haut degré de sophistication mathématique. Mais çà marche (et des compagnies gagnent de l'argent avec çà).
J'ajoute que, dans ces domaines, des équipes françaises jouent un rôle de tout premier plan.
Une référence (pour le compilateur) :
http://podcast.unice.fr/groups/conferences/weblog/dac19/Comment_faire_confiance_%C3%A0_un_compilateur___-_Xavier_Leroy.html
Voir aussi les cours de Gérard Berry au Collège de France.
@Sacha K
RépondreSupprimerJe croyais que l'un des théorèmes les plus importants en informatique, c'est qu'il est impossible de prouver qu'un programme est sans défaut. J'y voyais une conséquence du théorème de Gödel. Me trompé-je ?
Tu as parfaitement raison. Pour prouver qu'un programme est correct, il faut d'abord prouver qu'il s'arrête (et donc ne boucle pas indéfiniment) ; ensuite, qu'il donne bien le résultat cherché. Le résultat dû à Turing, et conséquence en effet du théorème de Gödel, c'est qu'il n'existe pas d'algorithme général pour déterminer si un programme s'arrête : c'est un problème indécidable. Mais le fait qu'il n'existe pas d'algorithme général n'entraîne pas l'impossibilité de la preuve pour tel ou tel programme particulier. La difficulté réside d'abord dans le fait de trouver un outil de spécification suffisamment puissant et précis pour exprimer ce qu'on veut que le programme fasse. Et ensuite dans la preuve proprement dite de l'équivalence entre la spécification et le programme réel, ce qui se fait généralement par étapes successives. En l'état actuel, chaque preuve est donc "sur mesure". Ce n'est pas demain qu'on pourra mettre de tels outils entre les mains de chacun. Mais quand on a prouvé une fois pour toutes la validité d'un noyau de système, on peut alors le mettre (par exemple) dans des millions de téléphones portables ou de commandes de freinage de trains, etc., et c'est ce qui a été fait. Deux articles me paraissent éclairants (ils sont par nature très techniques, mais peuvent donner une idée de la démarche) :
RépondreSupprimerXavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, July 2009.
Gerwin Klein (et 12 autres auteurs). seL4: formal verification of an operating-system kernel. Communications of the ACM, 53(6), June 2010
Une référence nettement plus accessible sur le noyau de système :
RépondreSupprimerhttp://www.ertos.nicta.com.au/research/l4.verified/