par Guillaume Connan
L’algèbre, qu’elle soit classique, générale ou linéaire, a pratiquement disparu de nos enseignements secondaires. Parallèlement, les probabilités et l’informatique occupent une place prépondérante. Cependant, l’informatique n’est que très timidement enseignée en tant que science. Un très rapide tour d’horizon devrait pouvoir mettre en lumière les liens étroits qui l’unissent à l’algèbre. Une approche plus rigoureuse de l’informatique apparaît alors comme un moyen d’offrir une nouvelle vie à notre chère algèbre si malmenée depuis quelque temps. De manière plus générale, l’introduction de mathématiques discrètes pourrait apporter une touche ludique, moderne et néanmoins rigoureuse à notre enseignement secondaire.
La version pdf est jointe en fin de l’article en ligne.
Voici quelques activités proposées à des étudiants de première année d’IUT d’informatique. Les étudiant(e)s viennent majoritairement de S. Le choix effectué par la plupart des IUT est de débuter par des mathématiques nouvelles pour la plupart : les mathématiques discrètes.
Il n’y a donc aucun prérequis d’analyse mais on a besoin de prendre un peu de recul sur les bases du calcul algébrique vu en collège. En effet, il s’agit d’étudier des ordinateurs ou, comme le disent les anglo-saxons, des computers c’est-à-dire des « calculateurs ».
Les étudiants sont également considérés comme novices en informatique : aucun prérequis dans ce domaine n’est exigé.
Les langages utilisés sont dans un premier temps OCaml qui a un fonctionnement très algébrique, comme nous allons le voir mais également Python, moins strict algébriquement, mais simple d’utilisation et permettant de manipuler simplement des objets de type matrice.
Définition récursive des ensembles : notion d’égalité, lois de composition
La notion d’ensemble est primordiale en informatique, en particulier en début de formation pour introduire les types de variables qui sont en fait des ensembles.
Voici une définition :
Un ensemble d’éléments est :
soit l’ensemble vide (noté {})
soit construit en « ajoutant » un élément à un ensemble. On notera x ⊕ E cette opération.
Cela se traduit par exemple en CAML :
Ainsi {3,{2,{1,Vide}}}
est l’ensemble contenant les entiers 1, 2 et 3.
Plusieurs problèmes algébriques apparaissent alors, le premier étant celui de la notion d’égalité de deux ensembles. On introduit alors l’axiome d’extensionnalité :
Les étudiants sont dès le premier mois confrontés à une avalanche de symboles « = » signifiant des choses bien différentes : égalité des contenus de mémoire, affectation, définition de variables et ici une égalité qui va contredire celle utilisée en mathématique :
La machine distingue $\{3,2,1\}$ et $\{2,3,1\}$ si l’on utilise l’égalité structurelle « = ». On a en effet utilisé la structure de couple ordonné pour définir un ensemble. On aurait pu utiliser la structure pré-existante « Set » qui aurait masqué ce problème. Cependant, en ce début de formation, il est important de bousculer les habitudes algébriques pour pouvoir prendre du recul et, pour des informaticien(ne)s, d’avoir en tête de ne pas avoir une confiance aveugle dans les réponses données par la machine.
Il va donc falloir créer différentes fonctions : une qui teste l’appartenance d’un élément à un ensemble, une autre qui calcule l’intersection de deux ensembles, une troisième qui teste l’inclusion. Le test d’égalité se résumera alors à un test de double inclusion.
Cette généralisation de la notion d’égalité va se poursuivre dans bien d’autres domaines : la congruence modulo un entier en arithmétique, l’équivalence de propositions logiques, l’équivalence d’automates, l’isomorphisme de graphes etc.
On en profite pour travailler sur l’inclusion en tant que loi de composition interne, munie d’un élément neutre mais tout le monde n’admet pas de symétrique.
L’autre problème est celui de la définition de l’opérateur ⊕ qui n’est pas commutatif et n’est même pas une loi de composition interne ce qui bouleverse les habitudes. Les élèves de lycée rencontrent bien la composition des fonctions mais de manière de plus en plus anecdotique.
Une égalité de ce type est donc perturbante :
en convenant de noter $x \oplus \{\} = \{x\}$.
Ainsi, une propriété comme la commutativité, semblant couler de source, est souvent pour la première fois mise en défaut algébriquement.
On découvre également de nouvelles propriétés d’opérations (qui sont introduites sur OCaml comme des fonctions) comme l’idempotence de l’union, de l’intersection, de la différence symétrique, la distributivité mutuelle de l’intersection et de la réunion : encore une habitude algébrique mise à mal (la multiplication des entiers est distributive sur l’addition mais pas l’inverse), les lois de De Morgan ou un « moins » devant une parenthèse transforme l’intersection en union (et non pas comme c’était l’habitude en l’intersection des « opposés » , etc.
Enfin la notion de fonction n’est plus liée à l’analyse mais devient un objet algébrique et de programmation : algèbre et informatique tissent leurs premiers liens étroits.
Après des années de pratique du calcul algébrique, il peut être en effet temps de prendre de la hauteur et de reconsidérer comme un cas particulier ce qui nous apparaissait comme une vérité générale. Les yeux s’ouvrent (ou devraient s’ouvrir) donc...
Lois de composition interne niveau II : logique des propositions / calcul booléen
Le chapitre suivant permet de généraliser encore plus la notion de calcul. Certains en ont déjà découvert un aspect avec l’étude du calcul booléen au lycée, en section ST2I et en S-SI mais avec leurs professeurs d’électronique et non pas en mathématique.
La première notion algébrique importante abordée est celle de formule bien formée. Disposant d’un alphabet constitué de propositions atomiques (représentées par la suite par des minuscules), de constantes logiques ⊤ et ⊥, de connecteurs ⋀, ⋁, → , ↔ et ¬ , de parenthèses « ( » et « ) » on définit l’ensemble des formules bien formées comme étant le plus petit ensemble F tel que :
– toute proposition atomique est un élément de F ;
– ⊤ et ⊥ sont des éléments de F ;
– si p ∈ F, alors ( ¬ p) ∈ F ;
– si (p,q) ∈ F² , alors (p ⋀ q), (p ⋁ q), (p → q), (p ↔ q) sont des éléments de F ;
– il n’y a pas d’autre expression bien formée que celles décrites précédemment.
Voici les étudiants confrontés au calcul non plus sur des nombres mais sur des propositions logiques : les voici capables de mécaniser une pensée simple. D’un point de vue plus pragmatique, on aborde de manière plus formelle qu’au collège des règles de calcul qui généralisent celles sur les nombres en disposant cette fois d’une présentation concise mais suffisante pour que le professeur ne soit plus celui qui dira si « on a le droit » ou pas d’effectuer tel calcul.
C’est aussi l’occasion de reparler de règles de priorité :
– ¬ a priorité sur les autres opérateurs ;
– ∨ et ∧ sont prioritaires sur → et ↔.
Cependant des expressions comme p ∨ q ∧ r demeurent ambiguës.
Le contexte informatique permet également d’introduire des arbres syntaxiques pour représenter des opérations.
Définissons tout d’abord sur OCaml un type de variables correspondant à nos définitions :
On peut alors se demander quelle formule représente :
Dessinons l’arbre correspondant à cette formule :
Il s’agit donc de
L’utilisation de calculatrices sur lesquelles on tape
les expressions comme on les écrit sur sa feuille induit depuis plusieurs années une perte de lien avec la construction arborescente qui est primordiale en calcul algébrique. Au collège on se demande « est-ce une somme ? Est-ce un produit ? ». Ici, les connecteurs sont plus nombreux et demandent plus de concentration.
Abstraction de la notion de calcul niveau III : étude d’un langage en tant qu’objet algébrique
Calculer sur un langage, voici une autre nouveauté qui pique la curiosité des étudiants. On est habitué à « dialoguer » avec un ordinateur via un clavier et un écran : comment faire ? Il est impossible d’aborder la théorie des langages et la compilation de manière sophistiquée. Cependant, la seule introduction en 1ère année suffit à voir une fois encore le calcul autrement. Une des grandes tâches de la machine est en effet de reconnaître des motifs : c’est la partie essentielle de la compilation, c’est-à-dire la traduction de programmes écrits dans un langage « humain » (Caml, C, Java, etc.) dans un autre, notamment le langage machine.
Un alphabet est un ensemble fini non vide. Les éléments sont appelés des symboles ou
des caractères.
Une chaîne est une juxtaposition de symboles. On appelle cette juxtaposition la concaténation.
Soit A un alphabet. Soit $\lambda_A$ la chaîne vide (ne comportant aucun symbole).
L’ensemble A∗ des chaînes construites avec l’alphabet A est défini par :
– $\lambda_A \in A^*$ ;
– si $a \in A$ et $c \in A^∗$ , alors la chaîne construite à partir de c en concaténant $a$ à droite est une chaîne de $A^∗$ ;
– μ est un élément de $A^∗$ seulement s’il peut être obtenu à partir de $\lambda_A$ par application de l’étape 2 un nombre fini de fois.
La concaténation des chaînes μ et ν est notée μν.
C’est l’occasion de parler de structures algébriques : la concaténation est une loi de composition interne sur $A^*$ car en concaténant deux éléments de $A^*$ , on obtient encore un élément de $A^*$.
Cette loi est également associative et possède un élément neutre $\lambda_A$.
Cela confère à $A^*$ la structure de monoïde libre, selon les standards informatiques (les mathématiciens parlent plutôt de magma associatif unitaire et les anglo-saxons de lattice).
C’est l’occasion de débattre sur l’utilité de distinguer certaines structures pour en connaître d’avance les propriétés.
L’associativité nous permet d’utiliser la notation puissance, mais de manière inhabituelle car nous ne disposons pas de la commutativité :
$a^n = aa...a$ ; $a^n b^k =aa...abb...b$ ; $(ab)^n =abababab...ab$
On définit des préfixes, des suffixes, des facteurs : par exemple bac est un facteur de aaabacaaa.
On définit une division partielle de chaînes : pour toutes chaînes μ et ν de $A^∗$ , le quotient à gauche de ν par μ est noté μ−1 ν et est défini par μ−1 ν = ξ si ν = μξ et n’a pas de sens si μ n’est pas un préfixe de ν .
On définit de même le quotient à droite. Si μ = aababc, le quotient à gauche de μ par aab est abc.
Les opérations affluent mais nous n’avons toujours pas parlé de langage : c’est simplement une partie de $A^∗$ . L’étude des langages va nous donner l’occasion d’introduire de nouvelles lois...
Cette fois, les lois ne portent pas sur les chaînes mais sur les langages : on peut en faire la somme (en fait l’union), le produit (en fait la concaténation) et une nouvelle appelée étoile de Kleene : l’étoile de Kleene du langage L est l’union sur tous les entiers k des Lk , Lk étant l’ensemble des chaînes de longueurs k construites avec l’ »alphabet » L...
C’est ici que ça commence à chauffer ! Il faut réaliser que pour la moitié des étudiants, après deux mois de cours, la notation $x^2$ est irrémédiablement associée au carré d’un nombre or ils ont été confrontés au carré d’une relation au sens de la composition, au carré d’un ensemble au sens du produit cartésien, au carré d’un symbole au sens de la concaténation et au carré d’un langage au sens de la concaténation des langages : des années à (mal...) manipuler des nombres ont profondément lié le calcul aux nombres.
À peine remis de leurs émotions suite à cet assaut de notations familières mais utilisées dans des contextes totalement nouveaux, voici une nouvelle définition et des conventions de notations :
Langage rationnel (ou régulier)
Soit L un langage sur l’alphabet A. Il est dit rationnel s’il peut être obtenu récursivement
uniquement à l’aide des opérations :
– réunion (somme),
– concaténation (produit),
– étoile de Kleene
en partant :
– du langage vide ,
– des langages du type $a$ avec $a \in A \cup \{\lambda_A\} $.
Considérons l’alphabet $A = \{b, o, x\}$ et L l’ensemble des chaînes finissant par x.
Par exemple, box, bobox, xxbobbxoxbbxxoxxxx, x appartiennent à ce langage.
On peut le décrire ainsi :
L = (b ∪ o ∪ x)* · x
C’est donc un langage rationnel car obtenu à partir de singletons et d’opérations rationnelles. Par abus de notation, on se contentera souvent de l’écrire ainsi :
Et tout ceci n’est qu’un début : viennent ensuite les notions d’expressions rationnelles, d’automates à états finis avec leurs nouvelles règles algébriques de calcul et de résolutions d’équations...
Réflexion sur la notion algébrique d’inverse : le calcul modulaire en arithmétique des entiers
L’arithmétique est présente à divers niveaux en informatique. L’étude est axée sur une initiation à la cryptographie : notions de groupe, anneau, corps pour aborder l’inversion, la résolution d’équations dans Z/nZ, les permutations pour le chiffrement par blocs.
L’arithmétique donne l’occasion de travailler pleinement sur les classes d’équivalences, avant de les revoir dans d’autres contextes informatiques comme lors de l’étude des graphes. Parler de classes d’équivalence permet de définir un nouveau type de variables si on y réfléchit en informaticien, ce qui permet d’éviter les confusions entre un entier et sa classe modulo n.
Par exemple, on peut définir le calcul modulaire sur CAML sous forme d’un enregistrement :
Ensuite, on crée un opérateur qui simplifiera notre saisie :
Par exemple, on peut définir la classe de 12 modulo 7 :
Ce n’est pas un entier, c’est une classe. Pour additionner les classes par exemple, on est obligé de définir une nouvelle opération :
Par exemple, la somme de la classe de 12 modulo 7 et de la classe de 15 modulo 7 s’obtient par :
En fait on peut créer une fonction d’ordre supérieur prenant l’opérateur en argument, d’une part pour économiser des copier-coller, d’autre part et surtout, pour monter d’un cran dans la modélisation algébrique, ce que permet un langage fonctionnel :
Alors par exemple :
On peut alors dresser la table de multiplication de ℤ/7ℤ et ℤ/8ℤ à la main ou avec la machine :
et on obtient :
ce qui permet de discuter sur l’existence de l’inverse d’un entier modulo n.
On peut ensuite le déterminer par une recherche exhaustive (on multiplie jusqu’à obtenir l’unité de Z/nZ ) ou en utilisant les coefficients de Bézout de l’algorithme d’Euclide étendu. Cela ouvre ensuite la porte à la notion d’anneau, de corps, du théorème d’Euler...
Permutations, cryptosystèmes par blocs.
Voici une activité ludique pour des collégiens et qui peut leur permettre de prendre du recul sur les résolutions d’équations : comment résoudre des équations dans des ensembles « bizarres » mais abordables ? Le ou exclusif et les permutations peuvent être introduits de manière simple sans rentrer dans un trop grand formalisme. On peut de plus leur fournir une table des codes ASCII des principaux caractères en b ase 10, leur demander de les convertir en base 2 puis d’appliquer le cryptosystème présenté ci-dessous.
Par exemple, « maman » sera chiffré en « eQ*yD » : c’est ludique et on fait des maths contemporaines...
Calcul polynomial pour multiplier des grands entiers sur machine
Une fois vu un algorithme naïf de calcul du produit de deux polynômes, on peut s’intéresser, naïvement aussi, au problème du calcul avec des grands nombres.
Par exemple, sur des machines 32 bits, certains calculs posent des problèmes. En effet, les entiers sont codés sur 31 bits plus un bit pour le signe : on ne peut donc pas dépasser $2^{31}-1$.
Prenons pour simplifier 123 456 789 × 987 654 321. On écrit chacun des deux nombres en base 1000 et on « remplace » les 1000 par des « X ». On est donc amené à effectuer le produit des deux polynômes $123X^2+456X+789$ et $987X^2+654X+321$. On obtient :
Il reste à remplacer les coefficients supérieurs à 1000 par des polynômes selon les puissances de 1000 :
$+(662X+382)X+253X+269$
On développe et on ordonne :
Le résultat est donc 121 932 631 112 635 269 : voici une activité qui peut également être menée au collège pour illustrer le calcul algébrique, la numération et le fait qu’une machine est limitée en mémoire et a donc besoin d’outils mathématiques pour aller au-delà de ses capacités basiques.
Il existe d’autres méthodes, notamment en utilisant le théorème des restes chinois, mais cela est un peu plus compliqué.
Compression et manipulation d’images avec des outils purement algébriques
La compression d’images est souvent présentée à l’aide d’outils analytiques issus de la théorie du signal et des probabilités. Il est pourtant possible de faire des manipulations assez efficaces aves des outils algébriques.
Une image sera pour nous une
matrice carrée de taille $2^9$ à coefficients dans $[~![ 0,
2^9-1]~!]$. Cela manque de charme ? C’est sans compter sur Lena
qui depuis quarante ans rend les maths sexy (la population hantant les
laboratoires mathématiques et surtout informatiques est plutôt
masculine ...).
Nous allons étudier pour cela la Décomposition en Valeurs
Singulières (SVD) qui apparaît de nos jours comme un couteau suisse des
problèmes linéaires : en traitement de l’image et de tout signal en
général, en reconnaissance des formes, en robotique, en statistique,
en étude du langage naturel, en géologie, en météorologie, en
dynamique des structures, en....
Il est bien sûr hors de propos de faire une étude poussée de la SVD au lycée mais qu’une matrice devienne une image et pouvoir faire quelques manipulations algébriques basiques mettent un peu de vie dans notre enseignement.
Nous allons travailler avec des images qui sont des matrices de
niveaux de gris. Notre belle amie Léna sera représentée par une matrice
carrée de taille $2^9$ ce qui permet de reproduire Léna à l’aide de
$2^{18}=262\,144$ pixels. Léna prend alors beaucoup de place. Nous
allons tenter de compresser la pauvre Léna sans pour cela qu’elle ne
perde sa qualité graphique. Une des méthodes les plus abordables est
d’utiliser la décomposition d’une matrice en valeurs singulières.
C’est un sujet extrêmement riche qui a de nombreuses
applications. L’algorithme que nous utiliserons (mais que nous ne
détaillerons pas) a été mis au point par deux très éminents chercheurs en 1965
(Gene GOLUB, états-unien et William KAHAN,
canadien, père de la norme IEEE-754). Il s’agit donc de mathématiques
assez récentes.
Matrices de niveaux de gris et Python
Python contient une matrice carrée de taille 512 contenant les niveaux de gris représentant Lena. Il suffit de cherger les bonnes bibliothèques :
l est donc un tableau carré de taille 512.
On peut préférer travailler sur une photo de format jpg (qui sera à l’envers) ou png (qui sera à l’endroit). Python la transforme en matrice avec la fonction imread. La matrice obtenue est en RVB : chaque coefficient est un vecteur (R,V,B). On la convertit en niveau de gris par exemple en calculant la moyenne des trois couleurs :
On obtient en fait Lena ou Marty tournée d’un quart de tour car on a transposé la matrice :
On peut tourner la photo de manière assez naturelle :
donnent respectivement :
Sachant que la palette de niveaux de gris en 8 bits part du 0 (noir)
vers 255 (blanc) :
On peut modifier le contraste en « mappant » par une fonction
croissant plus rapidement ou plus lentement que la fonction identité sur [0 ;255] vers [0 ;255].
Une matrice de taille $2^9$ contient $2^{18}$ entiers codés entre 0 et
$2^8-1$ ce qui prend pas mal de place en mémoire. Peut-on être plus
économique sans pour cela diminuer la qualité esthétique de la photo ?
La première idée est de prendre de plus gros pixels, c’est-à-dire une
matrice plus petite : on extrait par exemple régulièrement un pixel sur
$k$ (en choisissant $k$ parmi une puissance de 2 inférieure à $2^9$).
On peut également réduire le nombre de niveaux de gris en regroupant
par exemple tous les niveaux entre 0 et 63 en un seul niveau 0, puis 64
à 127 en 64, 128 à 191 en 128, 192 à 256 en 192.
Par exemple, avec 16, 8 puis 4 niveaux :
On peut être beaucoup plus efficace en utilisant la SVD.
En effet, la matrice image peut être décomposée sous la forme :
$
A = \sigma_1\cdot U_1\times {}^t V_1+\sigma_2\cdot U_2\times {}^t
V_2+\cdots+\sigma_r\cdot U_r\times {}^t V_r
$
avec les $\sigma_i$ de plus en plus petits. On peut donc approximer A
en ne gardant que les premiers termes de la somme sachant que les
derniers sont multipliés par des « petits » $\sigma_i$.
Le problème est d’obtenir cette décomposition. Python
heureusement s’en charge.
La somme obtenue n’est pas forcément entière. On utilisera alors la
fonction $\mathtt{floor}$ qui peut s’appliquer à un tableau entier.
Voici ce qu’on obtient avec 20, 50 et 100 termes dans la
suite.
La transmission d’informations a toujours posé des problèmes : voleurs
de grands chemins, poteaux télégraphiques sciés, attaques d’indiens,
etc.
Claude Elwood SHANNON (1916 - 2001) est un
mathématicien-inventeur-jongleur américain qui, suite à son article «
A mathematical theory of communications » paru en 1948, est
considéré comme le fondateur de la
théorie de l’information qui est bien sûr une des bases
de...l’informatique.
L’idée est d’étudier et de quantifier l’« information » émise et
reçue : quelle est la compression maximale de données digitales ? Quel
débit choisir pour transmettre un message dans un canal « bruité » ?
Quel est le niveau de sûreté d’un chiffrement ?...
La théorie de l’information de SHANNON est fondée sur des
modèles probabilistes : leur étude est donc un préalable à l’étude de
problèmes de réseaux, d’intelligence artificielle, de systèmes
complexes.
Par exemple, dans le schéma de communication présenté par
SHANNON, la source et le destinataire d’une information étant
séparés, des perturbations peuvent créer une différence entre le message
émis et le message reçu. Ces perturbations (bruit de fond thermique ou
accoustique, erreurs d’écriture ou de lecture, etc.) sont de nature
aléatoire : il n’est pas possible de prévoir leur effet. De
plus, le message source est par nature imprévisible du point de vue du
destinataire (sinon, à quoi bon le transmettre).
SHANNON a également emprunté à la physique la notion
d’entropie pour mesurer le désordre de cette transmission
d’information, cette même notion d’entropie qui a inspiré notre héros
national, Cédric VILLANI...
Mais revenons à Lena. Nous allons simuler une Lena bruitée de manière aléatoire :
Il existe de nombreuses méthodes, certaines très élaborées, permettant
de minimiser ce bruit. Une des plus simples est de remplacer chaque
pixel par la moyenne de lui-même et de ses 8 autres voisins directs,
voire aussi ses 24 voisins directs et indirect, voire plus, ou de la
médiane de ces séries de « cercles » concentriques de pixels.
Pour sélectionner des objets sur une image, on peut essayer de
détecter leurs bords, i.e. des zones de brusque changement de niveaux
de gris.
On remplace alors un pixel par une mesure des écarts des voisins
immédiats donnée par exemple par :
$\sqrt{ \left(m_{i,j+1}-m_{i,j-1}\right)^2+ \left(m_{i+1,j}-m_{i-1,j}\right)^2 }$
Enseignements
La liste des liens entre algèbre et informatique à un niveau élémentaire est encore longue : graphes, résolutions de systèmes, géométrie euclidienne, calculs en probabilités discrètes,...
Les quelques exemples évoqués suffisent à laisser penser que l’enseignement de l’informatique ne peut se faire sans des bases solides en calcul algébrique. Or l’informatique a été trop longtemps présentée dans l’enseignement secondaire comme un outil pour avoir de jolies figures ou des tableaux de gestion et pour nos élèves, elle n’apparaît pas vraiment comme une science à part entière. Certains collègues de mathématiques sont plus ou moins contraints de l’évoquer dans leurs cours mais surtout comme un outil d’illustration ou pour éviter de faire des calculs : il serait plus rassurant de constater que l’étude de l’informatique au contraire nécessite de faire des calculs.
D’un autre côté, la formation des étudiants en informatique ne pourra être que bancale s’ils ne disposent pas de bases solides en calcul. Les orientations des derniers programmes ne semblent pourtant pas aller dans ce sens. Cependant, des ouvertures pourraient exister, en MPS par exemple, où mathématiques et informatique sont trop souvent employées comme des outils secondaires mais pourraient au contraire devenir des objets d’étude à part entière et s’enrichir mutuellement.
On peut enfin rêver à l’introduction de mathématiques discrètes dans l’enseignement secondaire : cela permettrait de sortir des mathématiques du XVIIe pour rentrer dans celles du XXe avec peu d’outils et sans sombrer dans le catalogue de théorèmes et recettes non démontrées comme cela est trop le cas avec le nouveau programme de probabilités et de statistiques. Au contraire, avec très peu d’outils, mais de vrais outils, modernes et qui piquent la curiosité, on peut travailler différemment le calcul et découvrir des utilisations actuelles des mathématiques.
Citons pour finir un très grand informaticien parlant des liens entre mathématiques et informatique :
By now we all know that programming is as hard or as easy as proving, and that if programming a procedure corresponds to proving a theorem, designing a digital system corresponds to building a mathematical theory. The tasks are isomorphic. We also know that, while from an operational point of view a program can be nothing but an abstract symbol manipulator, the designer had better regard the program as a sophisticated formula.[…] Computing and Computing Science unavoidably emerge as an exercise in formal mathematics or, if you wish an acronym, as an exercise in VLSAL (Very Large Scale Apllication of Logic).[...]And from the mathematical community I have learned not to expect too much support either, as informality is the hallmark of the Mathematical Guild, whose members —like poor programmers— derive their intellectual excitement from not quite knowing what they are doing.[...]In the next fifty years, Mathematics will emerge as The Art and Science of Effective Formal Reasoning.
Edsger Dijkstra (1930 – 2002), prix Turing 1972, lors d’une allocution du 14 juin 1989 dont le texte manuscrit est disponible ici