kantien a écrit 1202 commentaires

D'après ce que wikipédia dit des systèmes structurels de types cela a l'air de correspondre.

En tout cas, moi je trouve la syntaxe concrète plus esthétique. Je ne trouve pas que le recours aux accolades pour délimiter les blocs et l'usage du point-virgule a tout bout de champ soit particulièrement joli. De plus, mettre un objet de type int dans une expression booléenne est surprenant sur le plan du typage (la transtypage 0 = false et true pour les entiers non nuls a son charme pour certain, moi je n'aime pas le mélange des genres). Le code qui s'approche de la manipulation des registres dans sa forme, c'est assez bas niveau : je préfère celui qui mime le principe même de l'algorithme d'Euclide pour le calcul du pgcd (on calcul le reste de la division euclidienne des opérandes, s'il est nul on renvoie le diviseur, sinon on poursuit avec le calcul du pgcd du diviseur et du reste : la traduction c'est l'affaire du compilateur). Enfin niveau performance, si l'on compile en natif, on se retrouve proche du C/C++.

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

Ou alors ils pourraient implémenter un système d'inférence de type à la Hindley-Milner ce qui leur permettrait de faire du duck-typing avec un typage statique et fort. :-)

(* définition avec annotations *)
let rec pgcd (a:int) (b:int):int =
  match a mod b with
  | 0 -> b
  | r -> pgcd b r
;;
val pgcd : int -> int -> int = <fun>

(* la même sans les annotations *)
let rec pgcd' a b =
  match a mod b with
  | 0 -> b
  | r -> pgcd' b r
;;
val pgcd' : int -> int -> int = <fun>
(* le système d'inférence s'en est sorti tout seul et a su typer correctement la fonction *)

(* je ne sais plus le type de la fonction, je demande à la boucle REPL *)
pgcd;;
- : int -> int -> int = <fun>

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

Tu n'as pas graissé les bons mots : « quand ça devient tendu ». ;-)

Comme je l'ai écrit dans un autre message, j'utilise rarement apt-cudf, les réponses d'apt-get me conviennent presque toujours.

Pour ce qui est des réponses qu'il fournit, tout dépend des critères d'optimisation que tu lui passes. Son utilisation, pour un contrôle fin, est sans doute plus compliquée que pour apt-get; ce qui doit expliquer la raison pour laquelle ce n'est pas le gestionnaire par défaut, outre son temps de calcul plus long. Et je ne connais pas de tutoriel pour expliquer, pas à pas, son fonctionnement de base. Pour les critères de base, il y a bien cette page sur le projet Mancoosi : MISC-2012 optimization criteria mais pour un utilisateur lambda cela doit paraître assez abscons.

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

Donc les tests montrent que ce nouveau solveur est vraiment mieux que tous les autres.
En plus l'un des auteurs a été DPL plusieurs années de suite et a donc une grande aura dans le projet Debian.
Question : pourquoi est-ce que apt ne passe pas en deprecated au profit d'aspcud et apt-cudf qui seraient installés par défaut ?

C'est une question que l'on peut légitimement se poser d'autant qu'un autre ancien DPL, en la personne de Lucas Nussbaum, a participé au projet Mancoosi. N'étant pas développeur Debian, je ne sais rien des discussions qu'ils ont pu avoir sur le sujet, mais je suppose qu'ils doivent avoir leur raison pour avoir laisser les choses en l'état. Personnellement j'utilise apt-get et ne bascule sur apt-cudf que lorsque la solution proposée par le premier ne me convient pas. Pour une administration quotidienne et « standard », apt-get fait bien son job et le temps de calcul est bien moins long (il ne s'attaque pas au même problème).

En revanche, les projets Edos et Mancoosi ont eu une incidence sur les processus d'assurance qualité chez Debian. L'étude du graphe de dépendance entre les paquets permet d'identifier les paquets qui ne sont pas installables, périmés ou critiques pour la distribution :

• Strong dependencies between software components
• Mining Component Repositories for Installability Issues
• Learning from the Future of Component Repositories
• Dependency Hell sur le wiki Debian.

Cela étant, en dehors du gestionnaire de paquets OPAM (Ocaml PAckage Manager) qui est un gestionnaire de paquets sources à la mode Gentoo, je ne connais pas de gestionnaires dont l'architecture est nativement construite autour d'un solveur SAT pour la gestion des dépendances.

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

En même temps, si tu n'utilises pas les bons outils pour ce genre de pratique free-style, il ne faut pas s'étonner si ça pose problème au niveau du gestionnaire de paquets.

Le solveur interne d'apt-get est une vrai bouse quand ça devient tendu (constat qui n'est pas propre au solveur d'apt-get, c'est le cas de la quasi-totalité des gestionnaires de paquets et pas seulement chez Debian), ce n'est pas un nouveauté, mais le problème de la gestion des dépendances est un problème ardu.

Lors du projet Edos qui se concentrait sur le problème spécifique de la construction de distribution linux, il a été montré en 2006 que le problème de la gestion des dépendances est un problème NP-complet par réduction à un problème de type 3-SAT (voir cet article].

S'en est suivi le projet Mancoosi étalé sur quatre années (de 2008 à 20011) qui a, entre autre, prolongé l'étude de cette problématique. Le projet a donné lieu a un concours de solveur SAT dont est sorti vainqueur le solveur aspcud. Le DPL de l'époque, Stefano Zacchiroli, a même mis au point un DSL pour les échanges entre les solveurs et les gestionnaires de paquets : CUDF.

Dans un article coécrit avec Pietro Abate, Roberto Di Cosmo et Ralf Treinen, ils proposaient une nouvelle architecture pour les gestionnaires de paquets : MPM, a modular package manager. Pour l'occasion ils ont juste développé un prototype en python qu'ils comparaient à apt, aptitude, cupt et smart dans des configurations constituées à l'époque de : sarge, etch , lenny, squeeze et sid (ils testent les 5 configurations en ajoutant progressivement chacun de ces dépôts dans le source.list). Pour ce qui est de trouver un scénario d'upgrade qui ne casse pas le système, le prototype a mis à l'amende tous ses concurrents ! :-)

Aujourd'hui, comment faire ? Installer aspcud et apt-cudf ! Pour se faire une idée de leur utilisation, on pourra se référer à ces articles sur le blog de Roberto Di Cosmo.

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

Effectivement, le livre n'explique pas le lien entre CPS et élimination des coupures : celui-ci est plutôt le fruit d'une réflexion personnelle en faisant un raisonnement par analogie via la correspondance de Curry-Howard. Cela étant, c'est plus une réflexion informelle qu'autre chose et il se peut que je pousse l'analogie au-delà de ses limites acceptables (ce n'est pas mon domaine de spécialisation, je ne suis pas informaticien théoricien).

Je vais détailler le schéma de pensée qui m'a amené à cette conclusion. Que dit la règle des coupures en théorie de la démonstration ? Elle généralise le principe du modus ponens : si A alors B, or A donc B. La forme générale de la règle des coupures est donné en bas de la page 11 dans le livre sus-cité : si j'ai deux séquents dans lesquels une même proposition A se trouve dans les prémisses de l'un et dans les conclusions de l'autre, alors je peux produire un séquent dans lequel celle-ci a disparue en fusionnant les prémisses et les conclusions. En haut de la page 12, cette règle est exprimée sous la forme particulière du modus ponens : si j'ai une preuve P1 qui a pour conclusion la proposition A, puis une preuve P2 dont la conclusion est la proposition B et dont A fait partie des prémisses, alors je peux produire une preuve P3 de la proposition B dans laquelle A ne fait plus partie des prémisses. Ensuite, la règle d'élimination des coupures affirme qu'il est également possible de produire une preuve P4 de la proposition B directement sans faire intervenir la preuve P1 qui produit la conclusion A ni la preuve P2 qui produit la proposition B lorsqu'elle a la proposition A dans ses prémisses.

Maintenant passons dans le monde des programmes via la correspondance de Curry-Howard. Cette dernière nous dit que chacune des preuves Pi correspond à un programme et les formules qu'elles manipulent sont les types des objets des programmes. Ainsi la preuve P1 produit un objet de type A qui est consommé par la preuve P2 pour produire un objet de type B ce qui, par coupure, fournit un programme P3 qui produit un objet de type B mais qui dans son exécution (par son recours à P1) doit allouer sur le tas un objet de type A (qui sera à terme désallouer par le ramasse-miette) : le modus ponens est la règle de typage de l'application de fonction :

let app (f:'a->'b) (x:'a):'b = f x;;
val app : ('a -> 'b) -> 'a -> 'b = <fun>

Mais, la règle d'élimination des coupures nous dit qu'il est possible d'écrire un programme P4 qui se passe totalement de cette allocation. Prenons maintenant l'exemple donné par Pierre Chambart dans l'article de blog chez OCamlPro pour calculer le minimum et le maximum d'une liste :

let rec fold_left f init l =
  match l with
  | [] -> init
  | h :: t ->
    let acc = f init h in
    fold_left f acc t

let keep_min_max (min, max) v =
  let min = if v < min then v else min in
  let max = if v > max then v else max in
  min, max

let find_min_max l =
  match l with
  | [] -> invalid_arg "find_min_max"
  | h :: t ->
    fold_left keep_min_max (h, h) t

Les types de ces trois fonctions sont :

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun>
val keep_min_max : 'a * 'a -> 'a -> 'a * 'a = <fun>
val find_min_max : 'a list -> 'a * 'a = <fun>

Icikeep_min_max joue le rôle de la preuve P1 (c'est un lemme qui est responsable d'allocation) et fold_left joue le rôle de la coupure qui produit la preuve P3 à savoir find_min_max. Puis dans la suite de l'article, en transformant son code via CPS, il produit la preuve P4 sans coupure find_min_max_k2 qui se passe d'allocation et qui aura la même fonction que la fonction find_min_max initiale si on lui passe comme continuation la fonction identité fun x -> x.

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

L'avantage d'utiliser un tableau est en fait celui de la Réification, on ne traite plus une méthode de calcul mais des valeurs. Par exemple si on veut tracer les courbes qui correspondent à la suite pour un n fixé, un nombre énorme de calculs seront refait plusieurs fois, alors qu'en ayant enregistré toutes les étapes intermédiaires, on ne refait jamais deux fois le même calcul, et le tableau se calcule en temps linéaire par rapport à sa taille.

Oui, c'est une manière comme une autre d'allouer sur le tas (en l'occurrence ici dans une matrice) ce qui autrement resterait dans la pile d'appel à chaque calcul de la fonction, ce qui revient à faire de la mémoïsation.

À l'inverse, dans certain cas, on peut vouloir éviter ce genre d'allocation pour gagner du temps de calcul lorsque l'on n'a pas besoin de réutiliser ultérieurement les données produites (traitement en flux) :
transformation CPS et réification de la pile d'appel
éviter les allocations en utilisant le paradigme Continuation Passing Style

Pour le rapport avec la preuve de la correction d'algorithme et la théorie de la démonstration, voir par exemple le livre Categorical semantics of linear logic aux pages 11-13 sur l'élimination des coupures.

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

C'est si gentiment demandé. :-) Bruno Michel t'as en partie donnée une réponse satisfaisante.

D'abord la citation que je donnais provient du site du benchmarck à la page why measure toy benchmark programms ?. Je la remets pour que ce soit clair, et le graissage n'est pas de moi mais se trouve dans la page original :

Non-motivation: We are profoundly uninterested in claims that these measurements, of a few tiny programs, somehow define the relative performance of programming languages.

Leur objectif, clairement affiché (« we are porofoundly unintersted »), n'est pas de se servir des résultats comme base pour determiner les performances relatives des différents langages. Visiblement, tu ne lui donnes pas le même objectif que ses auteurs.

Ensuite, passons à l'analyse d'un des tests, celui qui semble te préoccuper le plus : la gestion de la mémoire. Pour mettre à l'épreuve les GC, il y a le test binary trees

The work

The work is to create binary trees - composed only of tree nodes all the way down-to depth 0, before any of those nodes are GC'd - using at-minimum the number of allocations of Jeremy Zerfas's C program. Don't optimize away the work.

Le programme de Jeremy Zefra's, écrit en C donc avec gestion manuelle de la mémoire, est celui qui sert de référence et qui réalise le meilleur score du test

Maintenant, comparons ses performances face à deux langages avec GC :

Code source	temps	charge cpu
C gcc #3	3.26	59% 76% 78% 99%
Haskell GHC	25.62	36% 88% 49% 36%
OCaml #2	25.82	89% 95% 54% 64%
OCaml #5	41.55	1% 100% 1% 1%

Et là, on peut se dire : ces deux langages, avec leur gestion automatique, se prennent une valise ! M'enfin, OCaml a deux codes pour le test et avec un grande différence de temps entre le deux, pourquoi ? Alors, on regarde la charge CPU : le second est mono thread et pas le premier, donc déjà il y a une optimisation faite qui ne change rien au coût du GC et qui consiste dans la parallélisation des calculs. Mais au fait, n'y aurait-il pas d'autres code en C qui ont passé le test ? Et bien si, et voilà le résultat :

Code source	temps	charge cpu
C gcc #5	21.20	96% 89% 97% 97%

Tiens, on se rapproche déjà plus des performances de OCaml et Haskell ! Mais que ce passe-t-il donc dans ce code C par rapport au super code de la mort qui tue en 3.26 secondes ? Tout simplement il optimise bien moins le parallélisme. Il utilise pthread là où le plus rapide utilise apr-1.0.

Au final, les résultats du test (qui était sensé mettre à l'épreuve les GC) mais surtout en avant des optimisations de parallélisme. On trouvera les différents codes à ces adresses :

• code C gcc #3
• code C gcc #5
• code Haskell GHC
• code OCaml #2
• code OCaml #5

On pourra également noté que pour le code OCaml le plus rapide le parallélisme est fait à l'arrache (voir dans les commentaires : « Rough parallelization by Mauricio Fernandez »), que le code Haskell n'a pas le droit (c'est la règle du jeu) de profiter de son évaluation paresseuse (ce qu'aucun développeur ne fera dans du code réel) :

--
-- an artificially strict tree. 
--
-- normally you would ensure the branches are lazy, but this benchmark
-- requires strict allocation.
--
data Tree = Nil | Node !Int !Tree !Tree

et enfin que le code compilé OCaml ne profite pas de dernières optimisations apportées dans le compilateur par Flambda, contrairement au code C qui est compilé avec l'option -O3 de gcc.

Cela étant pour répondre à ta proposition de soumettre mon propre au code au test (qui devrait uniquement consister en une optimisation du parallélisme pour se rapprocher du haut du panier), j'ai autre chose à faire de mon temps que de jouer à « qui à la plus grosse ? ». Je suppose qu'il en est de même pour Fabrice Le Fessant, le fondateur de OCaml Pro, vu que c'est lui qui a soumis le code le plus lent (enfin, il a apporté des modifications sur le code d'un autre) : il sait pertinemment optimiser du calcul parallèle en OCaml, mais il doit avoir d'autres chats à fouetter.

Les benchmarks, c'est bien, encore faut-il en analyser correctement les résultats. ;-)

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

D'autant que sur un tel code, la définition de la fonction suit le schéma de la preuve par récurrence qui justifie son bon fonctionnement (c'est le principe même des langages fonctionnels, et des structures récursives).

Exemple en OCaml sur le calcul de la hauteur d'un arbre binaire :

type 'a btree = Empty | Btree of'a tree * a * 'a tree

let rec depth t = 
  match t with
  (* arbre vide, ou preuve de P(0) i.e on initialise la récurrence *)
  | Empty -> 0
  (* arbre à deux branches, ou preuve de P(n) => P(n+1) *)
  | Btree(left, _, right) -> (max_int (depth left) (depth right)) + 1

depth (Btree(Empty, 1, Btree(Empty, 0, Empty)))
- : int = 2

Dans ton cas, c'était une récurrence double et à la lecture du code il n'est pas difficile de se convaincre qu'il est correct. Sur des cas plus complexes, cela demande plus de réflexion, mais en fonctionnel cela reste plus simple.

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

C'est considéré comme une clause léonine ?

La clause d'un contrat est dite "léonine" lorsque les charges en sont supportées par une seule des parties alors que l'autre en tire tous les avantages. (Voir dans le domaine du droit des sociétés, le second alinéa de l'article 1844-1 du Code civil).

L'existence d'une telle clause dans un contrat ne le rend pas nul, la clause est seulement réputée non écrite.

Cela ne me choquerai pas, mais y a-t-il déjà eu des jugements allant dans ce sens ?

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

Il y avait de l'exagération volontaire dans mon propos. Je peux même comprendre, qu'en dehors du niveau A, SCADE puisse apparaître comme un char d'assaut (cela étant, en prenant en compte la nécessité d'avoir des développeurs formés à l'outil, le coût serait-il supérieur pour du niveau B ?).

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

Comparatif intéressant et sans doute plus impartial. L'article aurait pu s'intituler : « Quand la pratique peine à rejoindre la théorie ». :-)

En même temps, il y a peut être de la mauvaise foi non assumée chez une personne qui considère le benchmarkgame de chez Debian comme une « référence en terme d'optimisation » pour comparer les langages, là où pour les auteurs du comparatif ce n'est même pas le cas :

Non-motivation: We are profoundly uninterested in claims that these measurements, of a few tiny programs, somehow define the relative performance of programming languages.

source

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

Si j'étais cynique, je dirais que cela me fait penser à la scène de Fight Club dans laquelle Edward Norton explique son travail à son « amie à usage unique » au début du film : « Une voiture construite par ma société roule aux alentours de 90 km/h, le différentiel arrière se bloque. La voiture se crache est prend feu avec toute la famille à bord. Question : faut-il déclencher un rappel de ce modèle ? Prendre le nombre de véhicules concernés : A; le multiplier par le taux probable de défaillances : B; puis multiplier le résultat par la moyenne des sommes que l'on a été condamné à verser : C. A * B * C = X, si cet X est inférieur au coût d'un rappel : on ne fait rien. » :-/

Transposer le principe aux coûts de développements…

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

Je ne connaissais pas le principe, l'idée est intéressante ça mérite réflexion. L'idée est de déterminer « statiquement » les besoins en mémoire, non à la compilation, mais le plus tôt possible à l'exécution et ne plus faire d'allocations par la suite ?

Ce que tu décris sur la gestion des objets, n'est-ce pas justement le principe du RAII ?

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

Le troll sur le SC a déjà eu lieu, en voici le bilan (l'exemple devrait te plaire, le langage cible c'est ADA mais le code est généré automatiquement ;-)

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

Effectivement, si les listes sont de petites tailles ça ne vaut certainement pas le coup. Mais tes fichiers meta ne sont-ils pas un index de fichiers ? Une arborescence peut contenir plein de fichiers, ou alors tu as un index qui ne liste que les fichiers du répertoire et en général les répertoires ne contiennent pas assez de fichiers pour rendre intéressant le recours à la structure d'ensemble, c'est ça ?

Sinon pour faire du profilage d'utilisation mémoire à l'exécution tu as l'outil ocp-memprof développé par OCaml Pro qui permet d'analyser les fuites mémoires et de patcher le code coupable. :-) Pour développer ce genre d'outil il faut contourner le GC et même utiliser le module Obj, mais ce n'est pas le plus courant et il faut savoir ce que l'on fait.

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

Autre amélioration possible pour ton code : utiliser une structure d'ensemble plutôt qu'une liste pour ton type t.path. Les ensembles sont codés par des AVL et offrent une complexité logarithmique en temps là où avec tes listes tu as une complexité linéaire.

Ce qui donnerait pour le début de ton code :

module SS = Set.Make(String)
type t = { size : Int64.t ; path : SS.t}

cela te permettra, entre autre, de supprimer la fonction uniq et de coder merge_update ainsi :

let merge_update old new_ = { new_ with path = SS.union old.path new_.path }

tu n'auras plus besoin de générer une liste puis de la renverser, ou d'autres code dans le genre : la complexité en temps de tes algos sera grandement réduite.

Documentation du module Set et tutoriel succinct.

Tu vois : pas besoin de contourner le GC pour avoir du code efficace. ;-)

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

Si ça peut t'aider, j'ai rapidement deux remarques :

• quand on utilise toujours le même tampon, il vaut mieux utiliser Buffer.reset que Buffer.clean (voir la doc du module Buffer)

• tu parcours trop de fois le contenu de ton fichier : une fois pour le lire et le mettre dans une liste (via read_ic), une deuxième fois pour renverser la liste (toujours dans read_ic), et une troisième pour traiter chaque ligne avec decode (dans fast_read). Il vaudrait mieux le traiter en flux : voir le tutoriel sur les flux

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

Au passage… "Jane Street Capital" est une société de Trading, pas de "Fast Trading".

Il est vrai que cela fait une grande différence, et rend la solution avec GC acceptable.

Pour le reste, utiliser C/C++ est une question de bon sens : c'est le seul moyen d'exploiter à 100% les possibilités du matériel, toute approche avec GC bridant la puissance du matériel. À matériel équivalent, un GC n'égalera jamais une gestion manuelle, fine et bien faite.

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

Ça c'est la théorie. En pratique tu ne peux pas éviter d'avoir des allocations même dans la partie critique.

Une théorie qui ne correspond pas à la pratique, ou que l'on ne peut mettre en pratique c'est du vent : peut être de jolis mots mis les uns à la suite des autres, mais rien de plus (du blalba, en gros). Dit autrement, si ça ne vaut rien en théorie ça ne vaut rien en pratique et réciproquement.

Cela étant, dans la pratique, s'il y a bien un domaine où le temps c'est de l'argent c'est le trading haute fréquence (THF ou HFT). La latence peut coûter un paquet de pognon, mais les risques de bug encore plus; alors les acteurs de ce secteur font du calcul de risques (et ça, crois moi, ils savent faire ;-) entre le coût, les avantages et les défauts d'utiliser un langage avec GC pour leur back-end.

Et la société de courtage Jane Street qui gère 8 milliards de dollars et des millions de transactions par jour (2% de l'activité journalière de leur secteur) utilise OCaml pour leur back-end :

• pourquoi Jane Street utilise OCaml ?
• s'interfacer avec du C pour réduire la latence
• améliorer le GC pour réduire la latence

Les sociétés de courtage manqueraient-elles de pragmatisme ?

Sinon, je n'ai jamais croisé d'universitaire qui m'a soutenu qu'un système avec GC pouvait faire mieux que du C sur le plan de la latence (remarque de bon sens, un GC rajoute toujours de l'overhead).

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

Il faut toujours passer l'option -safe-string pour forcer la séparation entre les types string (immutable) et bytes (mutable), ce n'est pas encore l'option par défaut (pour ne pas casser, je suppose, le code existant qui utilise toujours le type string de façon mutable).

Il y a même des fonctions de conversions non sûres entre les deux types ce qui empêche Flambda de faire de la propagation de constante sur le type string.

Cela étant, je ne vois pas non plus ce qui empêche d'appliquer la méthode du C en OCaml pour le problème décrit par Nicolas. Il faudrait plus d'informations.

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

La gestation est arrivée à son terme ? J'espère pour ta femme que sa phase de travail n'a pas duré aussi longtemps. :-) Félicitations pour le petit (ou la petite).

Sinon pour faire une suggestion sur ton jeu. Dans ta dépêche tu demandes des retours sur les dessins vus de haut (personnages, autels…) et je trouve que cela rend assez bien, les arbres aussi. Par contre pour les terrains, la couleur uniforme (vert et marron) ça fait un peu « plat » et ça contraste avec les autres éléments. Ne pourrais tu pas voir avec David Tschumperlé pour faire des textures de terrains avec G'MIC ? Ça pourrait être sympa de voir deux projets, dont l'avancement est présenté régulièrement ici, coopérer.

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

Il y a d'autre part de la recherche en preuve pour les modèles distribués en utilisant des sémantiques de jeu, bien que cela soit au delà de mes compétences.

C'est à cela que je faisais référence, dans mon message à chimrod, quand je parlais du typage de protocoles réseau (et faire de la sémantique dénotationnelle dessus, en spécifiant la composition de deux protocoles à partir de leur sémantique respective ;-). Le lecteur intéressé pourra trouver un article, en français, sur la question sur hal où y sont exposés les principes de base de la démarche.

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

Mea culpa, je reconnais avoir été un peu sec dans mes réponses ce qui est un manque évident aux régles de bienséance, j'en suis désolé.

L'erreur est humaine, l'entêtement est diabolique (errare humanum est, perseverare diabolicum comme disent les latinistes), quelque soit le point sur lequel l'on se trouve pris en faute. Peu importe les torts réspéctifs de chacune des parties, l'important est la conciliation ou la réconciliation.

À l'origine de cette controverse, dispute ou discussion (choisis le mot qui te convient, peu m'importe) il y a effectivement, semble-t-il, une méprise. Je n'ai jamais, mais alors jamais, voulu dénigrer l'approche pragmatique par tests unitaires mais la critiquer, implicitement, cela est certain : mais la critique qui consiste à exposer les limites d'une méthode (ce qui sera à jamais en dehors de sa porté, et quand je dis jamais ce n'est pas parce que l'on ne sait pas faire aujourd'hui, mais parce l'on ne saura jamais faire certaine chose avec cette méthode, comme dans le théorème de Rice par exemple ;-) ne signifie pas le dénigrement (c'est nul, ça ne sert à rien et autres joyeusetés).

La pratique des tests unitaires est indispensable, comme approche, pour essayer de garantir le mieux que l'on peut que les programmes que l'on fait tourner sont corrects, dans la quasi-totalité des langage de programmation, et en OCaml particulièrement. Je n'aurai certainement pas contribuer à la rédaction de cette dépêche (la partie sur les améliorations du compilateur, avec chicco) si je considérai que la nécessité de reccourir à des tests unitaires en faisait un langage bon à mettre à la poubelle. ;-)

Le recours à des méthodes plus strictes et formelles pour garantir, avec certitude, qu'un code (ou un circuit) satisfait à ses spécifications n'est pas la panacée. Mais, contrairement à ce que tu crois, elles sont loin d'être un échec : et cela non uniquement dans les labarotoires de recherches, mais elles sont utilisées dans l'industrie depuis plus de vingt ans ! ;-) Et ce n'est pas le nombre d'acteurs industriels qui manquent : il me semblait avoir donné une liste importante dans ce message (et pas des moindres : IBM, Intel, Nasa, Agence Spatiale Européenne, Airbus…).

Pour te faire une meilleure idée de mes considérations sur les langages en informatique, je te propose la vidéo de cette conférence que j'avais abordée dans ma discussion avec chimrod.

Je me sens dans l'obligation de teaser un peu en commençant par sa conclusion : « j'espère avoir démonté l'idée qu'un langage est mieux que les autres, il y'en a qui sont moins bien que les autres ça c'est vrai, mais il n'y en pas qui sont mieux, il y a des choses différentes » (ce que j'exprimais, à ma façon, dans ce message en disant qu'il faut choisir l'outil adapté à ses besoins, ce qui nécessite de bien connaître ses besoins ainsi que les outils disponibles, leur qualités et leur faiblesses).

Il y a tout un passage tout à fait juste et assez comique sur les guerres de religion entre langage, dont voici la transcription de quelques diapos qu'il utilise :

L'imprératif

Détracteurs : l'impératif c'est un nid à bug, en particulier à cause des pointeurs et de la gestion mémoire par les utilisateurs

Partisans : Mais non, la programmation y est très naturelle, et il suffit d'y ajouter les assertions, les contrats, l'analyse statique, etc.

Le fonctionnel

Détracteurs : le fonctionnel, c'est pour les intellos, et c'est inefficace

Partisans : Mais non, ça demande juste un peu de culture scientifique, et l'inneficacité c'est du passé ! Le typage fort et la gestion automatique de la mémoire donne de la sécurité. Et on peut bien mieux raisonner sur les programmes, voire les prouver [là c'est moi qui graisse].

L'orienté objet

Détracteurs : L'objet c'est la fausse bonne idée : ça a l'air bien au début, mais il y a plein de problèmes (ex. héritage multiple) et c'est super-verbeux !

Partisans : Mais non ! l'héritage simple suffit le plus souvent, la programmation est naturelle et proche de l'architecture, elle passe bien à l'échelle, et le résultat est très efficace

La programmation logique qui a toujours était marginale

Détracteurs : La programmation logique et les contraintes, c'est bien joli, mais on ne sait jamais si ça va marcher et combien de temps ça va prendre !

Partisans (il précise « argument massue » dans la vidéo): Causez toujours, vous ne savez absolument pas faire ce que nous faisons !

Après avoir abordé les différents paradigmes, les principes du typage (dynamique ou statique) il conclue sur ces deux diapos :

Typage et vérification formelle

• Typage dynamique : arrêter l'éxécution en cas de d'opération illégale (choux + carotte)—Scheme, Python, etc.

• Typage Statique : dès la compilation, classifier les expressions selon les valeurs dénotées, et assurer la compatibilité des arguments des opérations

• Vérification formelle : dès la compilation vérifier des propriétés quelconques (cf. séminaire de T. Jensen) [NdM : séminaire qui suit le sien, où T. Jensen présente essentiellement un système d'annotations ajouter dans les commentaires de code Java, ce que gasche a présenté comme solution par invariants et préconditions]

Que peut-on savoir sur le programme sans l'exécuter, et à quel prix ?
Intuition : le typage doit être très rapide

À l'oral, comme commentaire à la question centrale de la diapo, il ajoute « et ça quand on fait des avions c'est assez utile. S'il fallait débuguer les avions en les crachants [NdM : approche tests unitaires] ce serait moyen comme idée, mais on le fait un peu sur les bagnoles » (se souvenir de Airbus dans la liste des industriels ;-)

Et celle-là qui classifie les niveaux et différents systèmes de typage

Niveaux de typage

1. Interdire choux+carottes
2. Typer les fonctions et leurs applications : C, Java, etc.
3. Typer l'ordre supérieur (fonctions de fonctions)
4. Accpeter les types polymorphes (paramétriques)
5. Sous-typage (langage objets)
6. Inférence de types : trouver les bons types même lorsqu'ils ne sont pas écrits par le programmeur
7. Typage de modules et APIs : Programming in the large
8. Niveau maximal actuel : Coq, cf. cours du 18 mars 2015, types dépendants, typage garantissant la terminaison, mais l'inférence générale n'est plus décidable

Enfin, plus tôt dans sa conférence, il fait une allusion au langage B et B-event de Jean-Raymond Abrial qui les a utilisé pour certifier du code pour la RATP dans les années 90 (en l'occurrence, ceux qui empreintes la ligne 14, en tête là où il n'y a pas de chauffeurs et où on voit devant soit, il y a un ordinateur qui fait tourner du code B ;-).

Et M. Abrial avait présenté cette histoire en 2015 dans cette conférence dont voici le texte de 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.

J'en extrairai juste trois diapositives :

la première en plein dans le sujet de la discussion

la RATP décide de supprimer les tests unitaires et d'intégration

Octobre 98 : lancement de la ligne 14

Depuis lors pas de problèmes avec le logiciel développé avec [soit 17 ans plus tard, et il tourne, tourne, tourne…]

pour remplacer la démarche par

86.000 lignes en ADA ont été produites automatiquement

27.800 preuves ont été faites

92% ont été prouvés automatiquement par l'Atelier B

Coût des preuves interactives : 7 hommes-mois

Les preuves interactives sont moins chères que les tests

Conséquence de cette première historique (date d'ouverture en 1998, rappelons-le, donc je te laisse imaginer depuis quand les ingénieurs utilisaient ces outils ;-)

Métros utilsant B pour leurs développements : New York City, Amérique du Sud, Europe, Chine, etc.

Projets plus récents en France avec B :

• Ligne 1 de la RATP à Paris (sans conducteur)

• Navette de l'Aéroport Charles de Gaulle (sans conducteurs, 158.000 lignes en ADA, 43.600 preuves, 96.7% auto)

J'espère avoir montré que ces méthodes de certification formelles (en grande partie automatisée) sont loin d'être un « échec », et t'avoir donné envie (ainsi qu'à d'autres) d'aller jeter un œil sur ces deux conférences.

Pour conclure, je citerai un extrait du message de Dinosaure et y avoir en partie satisfait :

Le deuxième point est ton apprentissage individuel. Les personnes qui composent la communauté OCaml sont souvent des chercheurs qui ont un savoir assez impressionnant (et qui dépasse souvent le simple cadre de la communauté OCaml) se qui fait qu'il est toujours intéressant de discuter avec ces personnes qui vont te pointer vers des documents qui t'en apprendront plus sur les langages informatiques (domaine de prédilection d'OCaml), les algorithme et les paradigmes. L'avantage est qu'on garde toujours une réalité de ces connaissances qu'on peut appliquer (et qu'on applique) dans l'industrie. Ce qui fait que même si la courbe d'apprentissage est rude, elle n'en est pas moins impossible - par exemple, je viens tout droit d'un milieu très industriel (et j'ai ignoré presque tout les aspects théoriques de l'informatique) et pourtant j'arrive à m'en sortir en comprenant des concepts que je n'aurais jamais eu la chance de voir dans le milieu d'où je viens.

Il est vrai que les chercheurs (ou ceux qui ont des connaissances approchantes) aiment bien aider, même s'ils peuvent se montrer susceptibles ou soupe au lait quand ils ont l'impression que l'on cherche à leur expliquer des principes théoriques qu'ils connaissent bien et considèrent comme triviaux.

Sur ce, j'espère qu'après ces échanges nous nous quitterons bons amis. :-)

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

Pas mieux !

On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.

et donc les argumentations diagonales à la Cantor ne s'appliquent pas.

À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification¹ (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.

Maintenant, on constate une technique du genre extension-restriction : le premier stratagème dans l'Art d'avoir toujours raison, avec un soupçon de « je mets de l'eau dans mon vin » sans en avoir l'air.

Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :

Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique)

Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F…), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.

Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.

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