kantien a écrit 1131 commentaires

L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80

Cela confirme une partie de la discussion qui suit la conférence : il semblerait que ce soit le bug d'Ariane V qui ait amené à s'intéresser à ce genre de technique.

Je ne me suis jamais penché sur la complexité de ce type d'algorithme, mais j'ai une question sur deux de tes remarques :

Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser.

et

Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique).

Les cas pathologiques pour la complexité exponentielle, on les rencontres dans du « vrai » code ? Je pose la question parce que, pour revenir sur le thème du journal et les ADT, ce système de type et son mécanisme d'inférence est basé sur l'algorithme d'unification de Robinson (milieu des années 1960) et le système Hindley-Milner ou le système F (début des années 70). Pour l'étude de la compléxité, il a fallu attendre 1991 et elle est doublement exponentielle. Xavier Leroy en propose une étude dans son livre sur le langage Caml (page 360 du livre et 370 du pdf). Cela étant, dans la « vraie » vie, sur du « vrai » code, on observe que l'algorithme se comporte linéairement : quand on double la taille du programme, on double le temps de compilation. Les pires cas en compléxité temporelle sont pathologiques; et à mon avis un programmeur qui les écriraient auraient soit l'esprit totalement tordu, soit aurait le cerveau qui exploserait bien avant de faire chauffer son CPU pour essayer de comprendre son propre code.

P.S : pour la vidéo, je les regarde en streaming via le lecteur proposé sur la page en question. Mais plus que la présentation des différentes techniques d'analyse statique, ce que je trouve intéressant c'est la discussion avec le public qui suit la présentation.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui, c'est bien la méthode B et l'atelier B qui est derrière tout ça. C'est un successeur du formalisme Z qui a inspiré le langage Eiffel et sa programmation par contrat.

Son inventeur, Jean-Raymond Abrial, est revenu sur l'histoire de ces approches dans une conférence au Collège de France dont voici la présentation :

Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Sur un simple enregistrement variant, l'information n'est pas portée avec le type dans la signature d'une fonction. Je peux comprendre qu'on puisse préférer que le compilateur refuse tout simplement de compiler lorsque la vérification est hors de portée.

Si la vérification est hors de portée du compilateur (avec une pleine certitude), alors il ne doit pas refuser de compiler (tout au plus, peut-il émettre un avertissement pour signaler ce qu'il ne peut savoir au cas où cela pourrait poser un problème au développeur) mais prendre des précautions en plaçant un test à l'exécution (ce qui semble être le cas).

J'ai réfléchi, depuis, à cet exemple en ADA et l'impossibilité pour le compilateur de suivre le bon typage d'une telle valeur vient peut être de sa mutabilité. Dans ton exemple, on voit bien qu'il y a là un problème. Mais, de ce que j'ai compris, cette variable pourrait se voir attribuer une valeur connue dynamiquement (après calcul d'une fonction par exemple) qui serait du bon type et possédant, cette fois, le champ en question.

Avec les ADT (même avec des valeurs mutables, comme en OCaml) ce n'est pas possible, car l'existence du champ est marquée par le constructeur de type qu'il faut nécessairement déconstruire.

type politique =
  | NbreFixe of int
  | NbreMaxHardware
  | PasDeThreading
  | CasParticulier;;

(* ici le terme est une variable mutable *)
let ma_politique = ref CasParticulier;;
let _ = ma_politique := NbreFixe 3;;

let i = match !ma_politique with
  | NbreFixe n -> n
  | _ -> assert false
val i : int = 3

Oups, désolé, je ne sais plus comment on a réussi à dériver d'une discussion qui par du compilateur Haskell pour finir par parler des langages objets. Toute mes excuses pour des propos qui auraient pu être interprétés comme blasphématoires dans ce fil de discussion de conviction plutôt fonctionnelle.

Il n'y a rien de blasphématoires dans ce fil, c'est toujours intéressant de voir comment une problématique peut être abordée dans d'autres langages et paradigmes. Et comme je l'avais signalé dans la dépêche sur le compilateur 4.03 de OCaml, c'est du code ADA qui fait tourner les lignes automatiques du métro parisien ;-) (même s'il n'a pas été écrit à la main, mais généré à partir d'un langage plus haut niveau).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Désolé si mon message a pu paraître agressif, telle n'était pas mon intention. C'est juste que je ne voyais pas où tu voulais en venir, ni le rapport avec les discussions du journal et des commentaires qu'il a suscités. Ma réaction était du même ordre que la fameuse réplique :

-- il dit qu'il a plus de genoux
-- il dit qu'il voit pas le rapport.

L'exemple central du journal tourne autour des garanties statiques que peut apporter Haskell (ou plus généralement, le système des ADT) pour la conception d'API et éviter les erreurs à l'exécution. S'en est suivi différentes discussions, avec des illustrations en ADA, Haskell ou OCaml, qui tournent toutes autour de ce même thème : peut-on (et si oui comment ?) contrôler la bonne formation des termes à la compilation (statiquement), ou doit-on mettre des gardes-fous et des tests lors de l'exécution (dynamiquement) ?

Ainsi lorsque je parlais d'outils d'analyses statiques, je ne considérais que ceux dont l'objectif se situe dans la gestion de cette problématique. C'est pour cela qu'à chacune de mes réponses, j'ai rappelé le contexte de la discussion. Je ne sous-entendais pas que les outils d'analyses de code se limitaient à gérer cette question. Et pour tous les cas d'usages que tu mentionnes, cela n'aurait d'ailleurs aucun sens d'avoir une alternative pour les traiter dynamiquement.

Une petite précision pour conclure :

Comme tu dis régulièrement que tu n'es pas développeur et que tu ne connais pas « l'industrie » ça ne me surprenait pas que tu ne connaisse pas ce pan là.

Il est vrai que je ne suis pas développeur (bien que je saches programmer, mais c'est loin d'être ma préoccupation première), et que je ne connais pas l'industrie. Mais quand je dis cela, c'est surtout pour exprimer que je ne sais pas ce qui est passé des laboratoires de recherche (et qui y est notoirement connu) vers le domaine industriel, ni le vocabulaire associé et le changement de dénomination qu'ont pu subir les notions lors du passage (ce qui est aussi parfois le cas lorsque la notion passe du domaine des mathématiques pures et de la logique à celui de l'informatique théorique).

Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :

Principe de l'analyse de programme :

• traduction vers un flux d'équation sur des ordres partiels
• résolveur général basé sur des itérations

et la méthode de résolution (comme il le souligne à l'oral) est en partie fondée sur des travaux de Tarski qui datent des années 1930. Résultats auxquels j'avais fait allusion dans un autre journal. Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.

Les résultats de Tarski me sont connus depuis une bonne quinzaine d'années (époque où j'étais étudiant), et ce genre de conférence me permet de savoir que des industriels peuvent en faire usage (quant bien même ils ignoreraient ce qui se trouve sous le capot, ou dans quel contexte et pour quelles raisons ces problèmes ont été résolus à une époque où l'ordinateur n'existait pas encore).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Dans le cas de l'attribut qui n'existe pas selon le discriminant, il n'y aura même pas de Waring à la compilation. Uniquement une Erreur au Runtime. Ça me semble difficile de détecter tous les mauvais usages d'un type variant, surtout si on peut récupérer le record depuis un contexte extérieur (non-Ada). Il faut bien que ça plante quelque part, au niveau de l'interface, si on fait de la programmation par contrat, ou plus loin dans le code si on ne teste pas à l'entrée.

Dans le cas où le code produit peut être utilisé via un autre langage qui ne permettrait pas de détecter statiquement l'erreur, assurément il faut bien alors mettre en place un contrôle dynamique avec émission d'une erreur. Cela relève du principe élémentaire dans le domaine réseau : « be conservative in what you send, be liberal in what you receive ». Ne sachant pas, a priori, ce que le code peut recevoir en entrée, il faut s'attendre à tout et être capable de gérer une erreur à l'exécution. Mais dans ton cas, le code est utilisé dans un contexte ADA et l'erreur est repérable statiquement. Détecter, dans ce cas, tous les mauvais usage d'un type variant à la compilation n'est pas une chose difficile : c'est le principe même du type checking, tâche qui incombe au compilateur dans les langages à typage statique.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Et justement, je dis que les analyseurs statiques servent aussi à refuser du code qui fonctionne parfaitement, mais qui ne correspond pas aux normes défini dans le programme en question par exemple.

Soit mais là on est un plus dans un problème de définition de terme : je ne dispute jamais des mots pourvu que l'on me dise le sens qu'on leur donne.

Mon commentaire était en réponse à un échange entre Guillaum et gerfaut83 au sujet d'un bout de code ADA et du comportement du compilateur. Guillaum s'étonnait de l'absence de garantie statique (absence d'erreur de typage à la compilation), ce à quoi gerfaut83 lui a répondu qu'on se trouvait à la limite entre le travail du compilateur et celui d'un analyseur statique.

Je réponds alors : le type checking (tache qui incombe au compilateur) c'est de l'analyse statique; et dans l'exemple donné il y a clairement un problème de typage qui peut être détecté statiquement, c'est-à-dire à la compilation. Puis j'illustre mon propos sur un exemple pour montrer en quoi cela peut être utile : réduire l'overhead à l'exécution. Comme la chose est vérifiée une bonne fois pour toute à la compilation, il n'est pas nécessaire de faire un test dynamiquement qui générera une exception.

Ensuite, répondre que l'on peut faire rentrer dans la catégorie des tâches dévolues à l'analyse statique d'autres problématiques que le contrôle d'erreurs est hors de propos. Généraliser le concept de l'analyse statique au-delà du cas d'étude ici discuté fait de ton objection une sorte de stratagème III : la généralisation des arguments adeverses :

Il s’agit de prendre une proposition κατα τι, relative, et de la poser comme απλως, absolue ou du moins la prendre dans un contexte complètement différent et puis la réfuter. L’exemple d’Aristote est le suivant : le Maure est noir, mais ses dents sont blanches, il est donc noir et blanc en même temps. Il s’agit d’un exemple inventé dont le sophisme ne trompera personne. Il faut donc prendre un exemple réel.

Exemple 1

Lors d’une discussion concernant la philosophie, j’ai admis que mon système soutenait les Quiétistes et les louait. Peu après, la conversation dévia sur Hegel et j’ai maintenu que ses écrits étaient pour la plupart ridicules, ou du moins, qu’il y avait de nombreux passages où l’auteur écrivait des mots en laissant au lecteur le soin de deviner leur signification. Mon adversaire ne tenta pas de réfuter cette affirmation ad rem, mais se contenta de l’argumentum ad hominem en me disant que je faisais la louange des Quiétistes alors que ceux-ci avaient également écrit de nombreuses bêtises.

J’ai admis ce fait, mais pour le reprendre, j’ai dit que ce n’était pas en tant que philosophes et écrivains que je louais les Quiétistes, c’est-à-dire de leurs réalisations dans le domaine de la théorie, mais en tant qu’hommes et pour leur conduite dans le domaine pratique, alors que dans le cas d’Hegel, nous parlions des ses théories. Ainsi ai-je paré l’attaque.

Les trois premiers stratagèmes sont apparentés : ils ont en commun le fait que l’on attaque quelque chose de différent que ce qui a été affirmé. Ce serait un ignoratio elenchi de se faire battre de telle façon. Dans tous les exemples que j’ai donnés, ce que dit l’adversaire est vrai et il se tient c’est en opposition apparente et non réelle avec la thèse. Tout ce que nous avons à faire pour parer ce genre d’attaque est de nier la validité du syllogisme, c’est-à-dire la conclusion qu’il tire, parce qu’il est en tort et nous sommes dans le vrai. Il s’agit donc d’une réfutation directe de la réfutation per negationem consequentiæ.

Il ne faut pas admettre les véritables prémisses car on peut alors deviner les conclusions. Il existe cependant deux façons de s’opposer à cette stratégie que nous verrons dans les sections 4 et 5.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Toutes les discussions que l'on voit au dessus montrent justement qu'il y a suffisamment de façon de résoudre un problème pour que ça ne soit pas figé dans le langage. Pour autant tu peux vouloir, au sein d'un programme donné, n'autoriser qu'une seule solution à fin d'améliorer la cohérence.

Où vois-tu dans mon propos que c'est figé dans le langage ? La discussion portait sur un bout de code ADA, celui-ci :

MaPolitique := (Politique => CasParticulier);
MaPolitique.NombreThread := 5; -- CONSTRAINT_ERROR : discriminant check failed

qui générera une exception à l'éxecution car, dans ce cas du variant, il n'y a pas de champ NombreThread. C'est là une problématique de typage, et d'ailleurs le compilateur semble savoir qu'il y a problème, mais la norme semble avoir préférée émettre un warning et non une erreur de compilation. D'où la question de Guillaum : « Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage ». Question à laquelle gerfaut83 a répondu : « J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code ».

D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ? D'où mon exemple pour refuser statiquement, par contrainte de type, un arbre vide comme entrée pour une fonction plutôt que de générer une exception à l'exécution; solution qui de plus réduit l'overhead du code généré.

Dans l'exemple ci-dessus, ce n'est pas tant une impossibilité d'inférer statiquement qu'il y aura un problème, mais un choix de la norme qui considère cela comme un avertissement et non comme une erreur critique. Mais dans bien des cas, sans ajout d'informations qui ne sont pas définies par le langage, il n'est pas possible de garantir certains invariants d'un code. Ce à quoi je faisais référence, pour aborder cette problématique, était des outils d'analyse statique comme JML pour Java présenté, par exemple, dans la conférence Intégration de la vérification formelle dans les langages de programmation.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

Certes, mais le contrôle de type (type checking) effectué par un compilateur relève de l'analyse statique de code. Dans les faits, on ajoute des outils d'analyse statique de code à l'extérieur du compilateur pour pallier aux déficiences du système de types d'un langage. Et pour fonctionner, ces outils nécessitent habituellement l'ajout d'annotations au code sous forme de commentaires, annotations qui correspondent à un enrichissement du langage des types du langage de départ.

Dans tout langage de programmation, il y a en réalité deux langages :

• le langage des termes pour décrire les calculs à effectuer ;
• le langage des types pour rejeter à la compilation, ou à l'exécution, certains termes comme sémantiquement invalides (vides de sens).

Plus le langage des types est évolué, plus il permet de contrôler la bonne formation des termes à la compilation (c'est-à-dire statiquement). L'idée des ADT est de pouvoir effectuer du raisonnement par cas non sur la valeur des termes (ce qui ne peut se faire qu'à l'exécution, là où la valeur est connue) mais sur leur type (ce qui est connu statiquement à la compilation).

On peut même pousser le principe plus loin avec des GADT pour discriminer plus fortement la construction des termes, et faciliter l'optimisation du code généré sans avoir à gérer d'exception au runtime. Je vais l'illustrer sur un exemple en OCaml avec une fonction qui retourne la valeur du nœud racine d'un arbre binaire parfait.

Avec les ADT, on peut encoder les arbres binaires parfaits ainsi :

type 'a t =
  | Empty : 'a t
  | Node : 'a * ('a * 'a) t -> 'a t

Les contraintes sur le type ne permettent que de construire des arbres parfaits : soit l'arbre est vide, soit c'est un nœud qui contient une valeur de type a et un arbre paramétré par un couple de type 'a * 'a (ce qui représente les sous-arbres gauche et droite).

Pour extraire, la valeur du nœud racine on procède ainsi :

let top = function
  | Empty -> failwith "Empty tree"
  | Tree (v, _) -> v

La fonction retournera une exception à l'exécution si on lui passe un arbre vide :

top Empty;;
Exception: Failure "Empty tree".

Maintenant, avec les GADT, on peut encoder ce type d'arbre ainsi :

type z = Z
type 'n s = S : 'n -> 'n s

type ('a, 'n) t =
  | Empty : ('a, z) t
  | Tree : ('a, 'n) t * 'a * ('a, 'n) t -> ('a, 'n s) t

Ici, c'est plus subtil et plus précis au niveau des contraintes de types. On commence par encoder les entiers dans le système de type avec z pour représenter zéro, et 'n s pour représenter la fonction successeur. Ensuite, on paramètre le type des arbres à la fois par le type des nœuds ('a) ainsi que par sa profondeur ('n). La définition dit qu'un arbre vide est de profondeur nulle et que les sous-arbres d'un nœud ont la même profondeur 'n (l'arbre est parfait) et que sa profondeur est 'n + 1 = 'n s.

Pour coder la fonction top, il est n'est plus nécessaire de traiter le cas de l'arbre vide :

let top : type a n. (a, n s) t -> a = function
  | Tree (_, v, _) -> v

Le type de la fonction déclare explicitement que la profondeur de l'arbre est du type successeur ('n s) et donc l'arbre ne peut être vide. Cette fois, si on lui passe un arbre vide, on a une erreur de typage à la compilation :

top Empty;;
Error: This expression has type ('a, z) t
       but an expression was expected of type ('a, 'b s) t
       Type z is not compatible with type 'b s

Pour ce qui est du code généré par le compilateur (option -dlambda du compilateur), on peut vérifier qu'il peut faire l'économie d'un test à l'exécution.

Avec ADT, on obtient :

let 
  (top =
    (function p
      (if p (field 0 p)
        (apply (field 1 (global Pervasives!)) "Empty tree"))))

Avec les GADT, on a :

let (top = (function p (field 1 p))

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Réserve partagée sur l'abus d'opérateurs ; cela dit, les parenthèses à la Lisp ne demandent pas de moindres efforts non plus.

C'est sans doute une question d'habitude. Je ne connais pas les règles de précédences des opérateurs infixes en Haskell mais, à partir des types des fonctions et des constructeurs, j'ai eu plus de facilité à lire ta version à celle avec parenthèses. J'ai du relire une deuxième (voire troisième) fois la version à la lisp pour bien me repérer; là où j'ai compris ton code à la première lecture.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Au temps pour moi, j'avais mal compris ce que tu voulais dire par là. Fréquentant peu le milieu des développeurs (que je lis surtout ici), je ne savais pas que les solutions orientées fonctionnelles étaient à la mode. De toute façon, les modes ça passe et ça repasse. ;-)

Cela étant, j'ai du mal à considérer les jugements disjonctifs et conjonctifs comme des notions sophistiquées. Ce qu'il y a, c'est qu'en POO la disjonction est abordée par la subdvision des concepts : l'héritage est un processus de spécification d'un genre (comme dans la proposition « un animal est un chien ou un chat ou une girafe… ») qui, comme l'a rappelé Guillaum, est ouvert par essence (nul ne peut dire a priori, c'est-à-dire statiquement, jusqu'où peut s'arrêter la spécification). L'avantage de la subdvision par les ADT est de fournir une partition exhaustive du type à diviser, et donc de pouvoir vérifier statiquement que tous les cas sont traités lors de la manipulation d'une valeur d'un tel type.

Comme l'a également rappelé Guillaum, les unions du C sont proches des ADT. Ce qu'il y a peut être de nouveau pour certains développeurs, c'est le vocabulaire employé pour qualifier ce genre de types : types de données algébriques. C'est lié aux relations que la disjonction et la conjonction entretiennent entre elles, et la façon dont elles opèrent l'une sur l'autre. Dans un choix comme celui d'un menu : (entrée et plat ) ou (plat et dessert), c'est équivalent au choix : plat et (entrée ou dessert). Ce qui n'est rien d'autre que la règle de distributivité de la multiplication sur l'addition : plat * (entrée + dessert) = (plat * entrée) + (plat * dessert).

En revanche, sur ce point :

Oui alors les types dépendants c'est une logique qu'un gamin de 4 ans comprends tout à fait.

je crois que tu surestimes grandement les capacités des enfants de 4 ans. ;-)

D'après mon expérience, un enfant de cet âge comprend tout à fait la logique propositionnelle (conjonction, disjonction et implication), c'est à dire celle qui sert de fondement au système de type de Haskell ou OCaml, mais ne sait pas raisonner si on introduit les notions de sujets et prédicats. Usuellement, on a plutôt fixé l'âge de raison à 7 ans; et encore même à 7 ans ce n'en est que des balbutiements.

Dans l'actualité récente, l'idée d'introduire les notions de sujet et prédicat dans les leçons de grammaire à partir des classes de CM1 a fait couler beaucoup d'encre : L'introduction du prédicat va-t-elle vraiment appauvrir la grammaire française ?. L'article est intéressant à lire, même si la notion n'est pas encore très claire pour son auteur. Comme dans l'exemple qu'il donne au début :

Par exemple, dans «cette polémique est totalement absurde», «cette polémique» est le sujet ; «est totalement absurde» est le prédicat, c’est-à-dire la partie de la phrase qui dit ce que le sujet fait ou est.

Ici le sujet est bien « cette polémique », mais le prédicat est « totalement absurde ». L'auxiliaire « être » constitue ce que l'on appelle la copule du jugement, c'est-à-dire la forme, là où le sujet et le prédicat en sont la matière. Comme dans le jugement suivant :

let l = [1; 2; 3];;
val l : int list = [1; 2; 3]

Le sujet est l, le prédicat int list et la copule est signifiée par le : entre eux. Ce que l'on exprimerait en français par la proposition : « la valeur l est une liste d'entiers ».

En revanche, les types dépendants ou leur forme affaiblie que sont les GADT ressemblent plus à des systèmes de types que je qualifierais de sophistiqués. Comme dans l'exemple suivant avec des GADT pour encoder la taille d'une liste dans son type.

module Llist = struct
  type z = Z (* zéro *)
  type 'n s = S : 'n -> 'n s (* la fonction successeur *)

  type un = z s (* un est le successeur de zéro *)
  type deux = un s (* deux est le successeur de un *)
  type trois = deux s (* trois est le successeur de deux *)

  type ('a,'n) t =
    | [] : ('a, z) t
    | (::) : 'a * ('a, 'n) t -> ('a, 'n s) t

  let rec zipwith :
    type a b c n. (a -> b -> c) -> (a, n s) t -> (b, n s) t -> (c, n s) t =
    fun f l l' -> match l, l' with
      | x :: [], x' :: [] -> (f x x') :: []
      | x :: y :: l, x' :: y' :: l' ->
          (f x x') :: zipwith f (y :: l) (y' :: l')
end;;
module Llist : sig
    type z = Z                                                                  
    type 'n s = S : 'n -> 'n s                                                  
    type ('a, 'n) t = [] : ('a, z) t | (::) : 'a * ('a, 'n) t -> ('a, 'n s) t   
    val zipwith :                                                               
      ('a -> 'b -> 'c) -> ('a, 'n s) t -> ('b, 'n s) t -> ('c, 'n s) t          
end

Ici on a des listes chaînées encodées via un GADT avec deux paramètres de types : a qui exprime le type homogène des éléments de la liste et n qui exprime la longueur de la liste (on encode les entiers dans le système de types via une représentation unaire, ce qui convient bien aux listes). Ainsi la fonction zipwith prend une fonction à deux paramètres et deux listes de valeurs, puis renvoie la liste des valeurs prises par la fonction. Mais ici, grâce au GADT, on peut exprimer dans le type de zipwith que les deux listes doivent être non vide et de même longueur (paramètre de type n s), sous peine de déclencher une erreur de typage à la compilation et non une erreur à l'exécution.

open Llist;;

let l : (int, deux) t = 1 :: 2 :: []
and l1 : (int, deux) t = 2 :: 3 :: []
and l2 : (int, trois) t =1 :: 2 :: 3 :: [];;

zipwith (+) l l1;;
- : (int, un s) t = :: (3, :: (5, []))

(* erreur à la compilation avec l de longueur 2 et l2 de longueur 3 *)
zipwith (+) l l2;;
Error: This expression has type (int, trois) t
       but an expression was expected of type (int, un s) t
       Type trois = deux s is not compatible with type un s 
       Type deux = un s is not compatible with type un = z s
       Type un = z s is not compatible with type z

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La question naïve c’est en quoi les ADT sont mieux que l’héritage et les méthodes virtuelles ?

La question pour moi, au départ, est : que cherche-t-on à exprimer ? Quelles sont les relations que l'on pense (avant d'écrire et exprimer sa pensée, il faut d'abord la constituer et la structurer) entre les structures de données ? Ici, il s'agit de rapport disjonctif et conjonctif : union disjointe et produit cartésien d'ensembles (comme dans le cas d'un menu au restaurant : entrée-plat ou plat-dessert).

Ces précisions faites, à ta question je répondrai : ADT ou héritage et méthodes virtuelles, relativement à la problématique exposée, c'est bonnet blanc et blanc bonnet. Le couple héritage et méthodes virtuelles est le moyen pour exprimer des ADT dans les langages orientés objets. La seule différence avec les langages fonctionnels, c'est que c'est plus verbeux. D'où ma conclusion : c'est quelque peu aberrant de devoir faire des circonvolutions pour exprimer une telle pensée.

type entree = (* ... *)
type plat = (* ... *)
type dessert = (* ... *)

type menu =
 | A : entree * plat -> menu
 | B : plat * dessert -> menu

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je sais que c'est moins hype que de décrire des typages sophistiqués, mais des factories font ça très bien.

Je ne vois pas en quoi l'approche par ADT est hype ou sophistiquée. Le principe même, à la base des ADT, consiste dans certaines formes logiques des jugements : la disjonction (exclusive) et la conjonction. Un jugement disjonctif, c'est hype et sophistiqué ? Quand un serveur, au restaurant, te demande si dans le menu tu as choisi l'option entrée et plat (conjonction, ou type produit) ou (disjonction ou type somme) plat et dessert, tu trouves cela hype et sophistiqué ?

Personnellement, ce que je trouve aberrant, c'est de devoir faire des circonvolutions pour exprimer des jugements de typage aussi triviaux et naturels à l'esprit humain.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pour rendre deux instances du type 'a P.t incompatibles, en choisissant des types incompatibles pour la valeur du type fantôme (int et float dans les exemples de octachron).

Dans l'usage des modules que j'ai proposé, on avait deux modules A et B dont les types étaient incompatibles : bien que structurellement identiques, comme ils étaient abstraits, les types A.t et B.t étaient incompatibles.

Dans l'approche avec type fantôme, il n'y a qu'un seul module et les types a P.t et b P.t sont rendus incompatibles par un choix adapté du type fantôme. Un des avantages que je vois, au premier abord, par rapport à ma solution, et que cela évite de dupliquer (dans deux modules distincts) les fonctions qui opèrent sur les types en questions. Tu pourrais, par exemple, définir deux type vides :

type abs (*coordonnées absolues *)
type rel  (* coordonnées relatives *)

puis faire un module de coordonnées :

module Coord : sig
  type 'a t
  (* signatures des opérations *)
end = struct
  type 'a t = int * int
  (* défintions des opérations *)
end

et définir tes variables avec des annotations comme cela :

let p_abs : abs Coord.t = (* ... *)
let p_rel : rel Coord.t = (* ... *)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

j'ai une M-Audio Fast Track Pro sous les yeux, qui déjà pour faire certains trucs (genre 24bit / 96kHz) sous Linux a besoin d'un driver spécial (donc PAS plug & play)

Eh, ça m'intéresse !!! :-) T'as un lien vers un tuto pour la faire fonctionner avec cet échantillonage ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire

Je pensais effectivement à l'encodage sous la forme des entiers de Peano. Comme c'est une représentation unaire des entiers, leur taille croît bien linéairement. C'est aussi cet encodage qui est illustré dans le cours de Jeremy Yallop.

L'idée est bien de montrer qu'avec les GADT, on peut avoir une forme affaiblie de type dépendant. Pour avoir des types dépendants complets, il faut passer à des langages comme Coq; mais là, c'est pour les fous ! :-P

Merci pour les deux liens, je regarderai cela à tête reposée.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je pense qu'il est souvent prématuré de se poser des questions de représentation mémoire quand on écrit un programme—à moins de savoir d'avance que le type sera impliqué dans les parties les plus coûteuses en performance.

C'est vrai, d'autant que j'ai parlé trop vite sur le coup mémoire. Là, s'il veut réduire les coûts, il peut garder son code actuel, enlever les parenthèses autour du couple dans sa définition de type et utiliser des fonctions de constructions là où il construisait en partant d'une paire existante.

depuis OCaml 4.04 (Novembre 2016), on peut écrire

type t = Foo of bar [@@unboxed]

pour supprimer l'indirection dans ce cas. (C'est utile pour packer des existentiels sans indirection.)

Je ne connaissais pas cette nouveauté, c'est intéressant.

Par contre, j'ai une question. Lorsque dans le journal, il s'interroge sur :

On peut (doit ?) pousser le concept plus loin, comme par exemple écrire une bibliothèque de calcul matriciel qui vérifie à la compilation la dimensionnalité des calculs.

Ce contrôle statique ressemble à des types dépendants (un type paramétré par une valeur du langage, ici un int pour la dimension des matrices). Pour ce cas, ça doit pouvoir se faire avec des GADT comme dans les exemples du cours de Jeremy Yallop; mais c'est un usage assez avancé du système de type. Me trompe-je ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il est vrai que la notation pour l'application des constructeurs de types inductifs peut apparaître contre intuitive, car elle n'est pas consistante avec celle des fonctions : c'est parce que en OCaml, on ne peut pas faire d'application partielle sur un constructeur de type (contrairement à Haskell, il me semble). Résultat les paramètres se passent entre parenthèses, comme en python par exemple.

Pour la taille mémoire, 5 ou 3 mots, cela se voit ainsi : un type somme occupe 1 mot mémoire qui contient des informations sur entre autre la structure des paramètres, plus 1 mot par paramètre. Ainsi dans le cas Coord of (int * int), on a 1 mot + 1 mot pour le paramètre qui pointe sur une paire int * int, paramètre qui contient lui même 1 mot de « tag » et 1 mot pour chaque int; d'où un total de 5 mots avec une indirection. Dans le cas Coord of int * int, on a 1 mot de « tag » plus 1 mot par paramètre, soit un total de 3 mots.

Si tu veux pouvoir créer une variable de type Coord of int * int à partir d'une paire préexistante, il faut passer par un «smart » constructeur, c'est-à-dire une fonction de qui prend une paire et renvoie une valeur du bon type (à l'instar de mes fonctions make dans mes exemples avec modules).

type coord = Coord of int * int;;
type coord = Coord of int * int

let coord (x,y) = Coord (x,y);;
val coord : int * int -> coord = <fun>

Sinon pour revenir sur l'approche modulaire, un de ses intérêts pourrait être, dans un premier temps, de te familiariser avec le système de module. Ensuite, tu pourrais jeter un œil sur les fonctions qui prennent des modules comme arguments pour retourner des modules, ce que l'on appelle des foncteurs. Comme ton projet consiste à afficher des schémas kicad, je vais comparer cela à l'électronique. Quand tu fais un schéma de circuit, certains composants peuvent être remplacés par d'autres tant qu'ils fonctionnement de la même façon : c'est cela un module, un composant. Et ton foncteur, c'est le schéma de ton circuit qui décrit comment les assembler pour fabriquer un nouveau composant. Si dedans tu as un micro contrôleur, tu peux opter lors de la réalisation entre des modèles de différents fabricants (qui peuvent différer sur leur structure interne) tant qu'ils réalisent la même fonction et exposent la même interface.

Si je reprends mon interface de coordonnées en lui ajoutant quelques fonctions :

module type Coord = sig
  type t
  val make : int -> int -> t                                                  
  val to_pair : t -> int * int
  val move : ?dx:int -> ?dy:int -> t -> t
  val compare : t -> t -> int
end

On peut l'implémenter avec des couples ou des paires (enregistrements) :

module PCoord : Coord = struct
  type t = int * int
  let make i j = (i, j)
  let to_pair p = p
  let move ?(dx = 0) ?(dy = 0) (x,y) = (x + dx, y + dy)
  let compare (i, j) (i', j') =
    let c = compare i i' in
    if c = 0 then compare j j' else c
end

module RCoord : Coord = struct
  type t = {x:int; y:int}
  let make i j = {x = i; y = j}
  let to_pair {x; y} = (x,y)
  let move ?(dx = 0) ?(dy = 0) p = {x = p.x + dx ; y = p.y + dy}
  let compare p p' =
    let c = compare p.x p'.x in
    if c = 0 then compare p.y p'.y else c
end;;

Comme ils définissent un type t et une fonction de comparaison compare, tu peux obtenir directement un module pour gérer des ensembles de coordonnées, en utilisant le foncteur du module Set de la bibliothèque standard :

module F = Set.Make(PCoord);;
module F :
  sig
    type elt = PCoord.t                                                         
    type t = Set.Make(PCoord).t
    val empty : t
    val is_empty : t -> bool
    val mem : elt -> t -> bool
    val add : elt -> t -> t
    val singleton : elt -> t
    val remove : elt -> t -> t
    val union : t -> t -> t
    val inter : t -> t -> t
    val diff : t -> t -> t
    val compare : t -> t -> int
    val equal : t -> t -> bool
    val subset : t -> t -> bool
    val iter : (elt -> unit) -> t -> unit
    val map : (elt -> elt) -> t -> t
    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
    val for_all : (elt -> bool) -> t -> bool
    val exists : (elt -> bool) -> t -> bool
    val filter : (elt -> bool) -> t -> t
    val partition : (elt -> bool) -> t -> t * t
    val cardinal : t -> int
    val elements : t -> elt list
    val min_elt : t -> elt
    val max_elt : t -> elt
    val choose : t -> elt
    val split : elt -> t -> t * bool * t
    val find : elt -> t -> elt
    val of_list : elt list -> t
  end

Tu peux voir ça comme si ton module offrait plusieurs pins en interface et que tu routes certains d'entre eux (le type t et la fonction compare) vers une partie de ton circuit pour avoir des ensembles. Mais dans la pratique, tu peux choisir un modèle de composant plutôt qu'un autre pour des raisons de performance (bien que dans mon exemple bateau, les deux doivent être sensiblement identiques une fois compilés).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pas forcément, ça dépend de la manière dont le type est écrit. […]

Intéressant, je ne savais pas qu'il y avait une différence entre les deux écritures au niveau de la représentation mémoire. Je croyais qu'au niveau du compilateur, il y avait juste des passes d'optimisation au niveau des phases de constuction-deconstruction pour réduire le nombre de suivi de pointeurs. Et cette « curryfication » des constructeurs, elle est faite pour tous les types de tuples ?

Edit : c'est bon, j'ai ma réponse dans ton commentaire en réponse à Aluminium.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il existe un autre moyen, pour éviter les alias entre types structurellement identiques, qui consiste à passer par le système de modules et les type abstraits. Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire : tes types sont des pointeurs sur des couples de int (qui n'ont pas la même étiquette et ne sont donc pas identiques). Afin d'éviter ce pointeur, on peut utiliser des modules dans lesquels les types seront directement des couples mais en le cachant au monde extérieur.

Exemple :

(* on définit une signature pour un module de coordonnés *)
module type Coord = sig
  type t
  val make : int -> int -> t
  val to_pair : t -> int * int
end

(* on définit deux implémentations identiques *)
module A : Coord = struct
  type t = int * int
  let make i j = (i,j)
  let to_pair x = x
end;;
module A : Coord

module B : Coord = struct
  type t = int * int
  let make i j = (i,j)
  let to_pair x = x
end;;
module B : Coord

Ici, comme l'interface des modules définit un type t sans rien dire sur lui (on parle de type abstrait), les types A.t et B.t sont incompatibles, bien que structurellement identiques.

let p = A.make 1 2;;
val p : A.t = <abstr>

A.to_pair p;;
- : int * int = (1, 2)

(* les types ne sont pas compatibles *)
B.to_pair p;;
Error: This expression has type A.t but an expression was expected of type B.t

Ensuite, il est aisé, à partir des primitives des modules, d'écrire des fonctions de conversions d'un type dans l'autre :

let a_to_b x = let i,j = A.to_pair x in B.make i j;;
val a_to_b : A.t -> B.t = <fun>

let b_to_a x = let i,j = B.to_pair x in A.make i j;;
val b_to_a : B.t -> A.t = <fun>

let p1 = a_to_b p;;
val p1 : B.t = <abstr>

B.to_pair p1;;
- : int * int = (1, 2)

A.to_pair (b_to_a p1);;
- : int * int = (1, 2)

P.S : tout système de types, quelque soit le langage, a à voir avec la preuve de programme, mais là c'est une autre histoire. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

D'ou ma question, est-ce que tu peux me dire en quoi je ne lui rends pas justice ?

Je réponds ici de mon point de vue, et de la façon dont j'avais perçu sa méthodologie et ses principes suite à la présentation de ton journal. S'il est vrai, qu'en conclusion de ton paragraphe sur le sujet, tu précises qu'il y a des règles établies et que le rôle des mainteneurs est de veiller à leur respect; il y a néanmoins un passage qui peut induire en erreur (ce qui fut mon cas) sur la compréhension de ses principes :

Par conséquent, lorsqu'on réalise un projet communautaire, toute contribution est bonne à prendre. Il nous invite à donc à être laxiste sur les conditions d'acceptation d'un patch.

Lorsque je lis ce texte, cela m'apparaît être le contre-pied de ce que l'on trouve dans le C4 (Collective Code Construction Contract). Il désirait effectivement que tout le monde puisse devenir contributeur :

Everyone, without distinction or discrimination, SHALL have an equal right to become a Contributor under the terms of this contract.

Cependant, l'existence même de ce contrat impose des conditions d'acceptabilités pour une contribution, là où ta formulation laissait sous-entendre que c'était totalement inconditionné et même laxiste. Les huit règles rangées sous la catégorie patch requirement me semble relever de tout sauf du laxisme. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Disons que l'on ne sait pas trop ce qu'il faut entendre par pur littéraire.

Mais des littéraires (si l'on entend par là des personnes qui ont suivie des études dites littéraires) qui étudient l'informatique et les mathématiques, cela existe indubitablement. Lorsque j'étais encore étudiant, j'ai suivi une formation intitulée : Logique mathématique et fondement de l'informatique. Parmi les étudiants, la grande majorité était issue d'un cursus de mathématique, mais certains venaient de la philosophie. En particulier une étudiante, détentrice d'un bac littéraire et d'une maîtrise de philosophie, qui, au cours de sa thèse, enseigna l'algorithmie et la programmation en faculté.

Il y a aussi, par exemple, Baptiste Mélès, auteur d'un article sur le site images des maths du CNRS (article qui traite de l'implémentation d'un algorithme de division sur une machine à registres limités, plus connu sous le nom de boulier) et qui, d'après son curriculum vitae, a eu un bac L, est passé par une prépa littéraire, a fait l'ENS, une licence en lettres modernes…

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est ça. Sauf que la représentation intermédiaire n'est pas toujours totalement agnostique.
Celui de llvm est particulièrement bien documenté (pour un langage intermédiaire), c'est parce qu'il est considéré comme une interface du compilateur (alors que gcc considère ça comme une représentation interne). Un petit peu de lecture : https://en.wikipedia.org/wiki/LLVM#LLVM_intermediate_representation

C'est ce à quoi je m'attendais.

Pour moi, un compilateur c'est une fonction qui prend en entrée un texte écrit dans un langage et qui renvoie un texte écrit dans un autre, tout en préservant certains invariants dont le plus important est la sémantique du code. En gros : c'est un morphisme avec certaines propriétés qui sont propres aux compilateurs.

Dans les faits, pour écrire ce morphisme, on le décompose en fonctions distinctes et séparées aux rôles spécifiques, et on l'obtient par composition. Que certains groupes de fonctions se nomment backend et frontend (voire middle-end d'après la réponse de lasher) était le sens de ma question initiale. Cela semble relever du vocabulaire du génie logiciel, soit de l'ingénierie, vocabulaire que je ne connais pas spécialement.

Après, une représentation intermédiaire, pour moi, c'est juste le domaine d'arrivée (puis de définition) d'une des fonctions qui composent le compilateur. Dans des compilateurs comme GCC ou LLVM, qui prennent une multiplicité de langage sources en entrée et une multiplicité d'architectures cible en sortie, il faut bien à un moment donnée un langage commun, pivot; ce qui semble être le rôle du langage succinctement décrit, pour LLVM, dans le lien wikipédia que tu as donné.

Si si c'est juste que tes postes volent trop haut pour quand je suis en vacances ^ ^

Arf désolé, j'essayes de me retenir pourtant et je ne pensais pas que celui-ci volait si haut que cela. La conférence de la vidéo est surtout une conférence d'histoire de la logique et de l'informatique théorique au cours du XXème siècle. Je l'ai trouvé sur la page history of logic and programming languages sur le site de Philipp Wadler. Mais si j'en juges à la note de mon commentaire, la science et l'histoire des sciences ne semblent pas intéresser grand monde ici, à moins (ce qui est sans doute plus probable) que ce ne soit mon sens de l'humour qui ne fasse rire que moi.

Dans le même genre (compilation et histoire), il y a l'article (de vulgarisation, rien de bien théorique ni de très pointu dedans) la comptine des neufs divisions sur le site images des maths du CNRS. Son chapeau est :

Les calculateurs chinois ont fait usage d’une « table de division » qui, tirée de son contexte, peut sembler mystérieuse. Mais tout s’éclaire aussitôt qu’on la lit comme une liste d’instructions pour le boulier.

Il parle d'une comptine que les enfants chinois apprenaient pour pratiquer la division sur un boulier, qui n'est autre qu'un algorithme de division pour un machine (non automatisée) avec un nombre de registres limités, plus connu sous le nom de : boulier. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Après mon rêve à moi c'est plutôt les langages que les compilateurs, et j'aurais tendance à m'intéresser plutôt aux langages qui font des choses chouettes, même quand leur backend est un peu simple (OCaml, Haskell)

Au passage un message totalement hors-sujet, tant que je te vois dans les parages.

Il y a un projet de dépêche en cours de rédaction sur le thème Outils de développement OCaml par une personne venant de terminer le MOOC OCaml. Peut être pourrais tu y apporter ta contribution si tu as du temps, tu connais mieux le sujet que moi, en particulier sur la partie consacrée à Batteries. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Merci pour ces précisions, je comprends mieux à quoi faisait référence les termes backend et frontend.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Grosso modo, le frontend décode le source pour en faire un code intermédiaire qui sera traduit dans le langage de destinataion par le backend.

Merci pour ces précisions. Si je comprends bien, il y a un langage intermédiaire (agnostique vis à vis du langage source) que cible le frontend, puis le backend part de cette représentation intermédiaire pour traduire vers le langage cible qui dépendra de l'architecture machine. C'est cela ?

Je te laisse troller sur les langages, je vois pas le rapport avec la compilation :)

C'est pas du troll, c'est une boutade. ;-) Même avec des emoticônes, le second degré ne passe pas sur linuxfr ?

Ce n'est pas, directement, en rapport avec la compilation, mais avec la fin du message de gasche. Et deux des langages qu'il cite (OCaml et Haskell) dérivent explicitement du lamba-calcul. D'ailleurs gasche est relecteur des patchs soumis sur le compilateur OCaml et a les droits de commit sur le dépôt, et Philipp Wadler est un des grands contributeurs au langage Haskell et l'implémenteur de generics en Java (ça c'est pour toi, il me semble que c'est le langage que tu utilises le plus; et dans la vidéo il explique d'où vient l'idée ;-).

En tout cas, la vidéo a bien un lien avec le thème du journal : quand on s'occupe de faire un langage et d'écrire un compilateur, il vaut mieux bien maîtriser la théorie. Et cette théorie, elle vient d'une source principale : la logique mathématique et la théorie de la démonstration. ;-)

Par contre, je me suis trompé pour la vidéo où il montre un extrait d'un article de Turing, c'est celle-ci (mais le contenu des deux conférences est similaire). L'article date de 1937 et l'abstract est :

Computability and lambda-definability

The identification of "effectively calculable" functions with calculable functions is possibly more convincing than an identification with the lambda-definable or general recursive functions. For those who take this view the formal proof of equivalence provides a justification for Church's calculus, and allows the "machines" qhich generates functions to be replaced by the more convenient lambda definitions

Enfin si tu ne vois pas le rapport à la théorie des langages (et donc in fine avec la compilation), c'est peut être que tu n'en connais que succinctement le contenu, ou que tu ne connais pas le contenu de philosophie kantienne. ;-)

Juste une illustration, dans un article de 1905, au cours d'une polémique qui l'opposait avec des logiciens comme Russell ou Hilbert, Henri Poincaré écrit en introduction :

Pour M. Couturat, la question n'est pas douteuse : ces travaux nouveaux ont définitivement tranché le débat, depuis si longtemps pendant entre Leibniz et Kant. Ils ont montré qu'il n'y a pas de jugements synthétiques a priori, que les mathématiques sont entièrement réductibles à la logique et que l'intuition n'y joue aucun rôle.

C'est ce que M. Couturat a exposé dans les articles que je viens de citer; c'est ce qu'il a dit plus nettement encore à son discours du jubilé de Kant, si bien que j'ai entendu mon voisin à demi voix : « on voit bien que c'est le centenaire de la mort de Kant ».

Puis continuant, à la fin de son introduction il émet une très très grande objection au travaux des logiciens qui lui étaient contemporains :

Nous venons d'expliquer l'une des conditions auxquelles les logiciens devait satisfaire et nous verrons plus loin qu'il ne l'ont pas fait.

Et pour cause : ils ne pouvaient pas la satisfaire; et cette impossibilité devait être prouvée, par Gödel, 26 ans plus tard¹ sous le nom de théorème d'incomplétude ou, dans la version de Turing, indécidabilité du problème de l'arrêt.

Donc qui avait raison ? Kant et Poincaré ! ;-)

Tout ça pour dire : l'ordinateur, les langages de programmations, l'informatique, ce n'est pas venu du jour au lendemain dans la tête de Turing. Ça s'inscrit dans une tradition historique qui relève de la logique, de la philosophie et des fondements de mathématiques : c'est ça les bases théoriques des langages de programmation. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.