kantien a écrit 1131 commentaires

Et tu fais quoi des agneaux ?

Faudrait demander à Michael Kael.

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

Ma sœur, qui travaille au CNAM, m'a ramené cet été son « Manuel d'écriture inclusive » gracieusement offert par la direction à ses employés (elle savait que ça me plairait, et je dois dire que quand je veux rire un bon coup, je le feuillette).

Ce manuel écrit par l'équipe de mots-cles vaut le détour et contient de magnifiques perles dont celle-ci :

Le point milieu permet d'affirmer sa fonction singulière d'un point de vue sémiotique et par là d'investir « frontalement » l'enjeu social et discursif du rapport femmes / hommes.

Je constate, avec regrets, à quel point les commentatrices et commentateurs de linuxfr ne perçoivent pas assez cette fonction singulière d'un point de vue sémiotique du point milieu. :-P

Dans le style jargon pédant, ils font fort ! Mais là où c'est le plus risible, dans la cohérence de la démarche, est que l'on peut lire sur la page précédente :

Le point milieu nous semble ainsi préférable au parenthèses (qui, en usage, indique un propos secondaire), à la barre oblique (qui connote une division) […]

Voici donc la barre oblique qui, d'un point de vue sémiotique, connote une division mais que l'on utilise une page plus loin sous la forme : « rapport femmes / hommes ». Va comprendre !

On notera également qu'il serait préférable d'employer l'expression « Droit de la personne humaine » en lieu et place de celle de « Droits de l'Homme » (qui fait usage de l'antonomase¹ du mot commun « homme »). Le pléonasme personne humaine est sans doute là pour faire la distinction d'avec les personnes canines, ce qui, soit dit en passant, pose un problème d'exclusion vis à vis des lycanthropes. :-P

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

C'est étrange, normalement le tas mineur a une taille de 2M sur une plateforme 64-bits, un fichier de quelques ko y rentre sans problème. Si tu traitais tes fichiers séquentiellement dans un boucle, je ne vois pas ce qui empêchait le GC de les collecter sans les envoyer dans le tas majeur. En revanche si tu commençais par lire tes 10_000 fichiers, puis que tu les traiter ensuite un par un, là effectivement tu devais solliciter beaucoup plus le GC. Mais dans ce cas ce n'est plus du tout le même algorithme qu'avec un char[] en C ou C++.

Sinon, pourquoi ne pas utiliser un buffer tampon de taille fixe comme tu l'aurais fait en C ou C++ ?

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

Si il y a plein de string partout, cela va bien plus vite, par contre, si il y a plein de string à vie courte, la consommation mémoire s'envole, car il est impossible de réutiliser un buffer.

Pourquoi la consommation mémoire s'envolerait avec des string à vie courte ? Le tas est en deux parties : le tas mineur de taille fixe pour les petits objets à vie courte et le tas majeur redimensionnable pour les objets à vie longue. Le comportement mémoire dépendra du ratio entre le taux de création des string, leur taille et leur durée de vie, mais il est probable qu'elles ne quitteront jamais le tas mineur et seront collectées sans avoir besoin d'être promues dans le tas majeur, seule situation qui pourra provoquer l'allocation de mémoire supplémentaire.

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

Rust n'a pas de GC, mais un système de propriété des variables qui est très marrant à utiliser.

Il me semble qu'il y a avait un GC dans les débuts de Rust, puis ils l'ont retiré. Felix Klock (membre de l'équipe en charge des nouvelles fonctionnalités du langage) a écrit une série d'articles intéressante sur le sujet :

• GC and Rust Part 0: Garbage Collection Background
• GC and Rust Part 1: Specifying the Problem
• GC and Rust Part 2: The Roots of the Problem

Pour ce qui est du multi-cœur en OCaml, c'est justement le GC qui pose problème. Xavier Leroy et Damien Doligez avaient écrit un article en 1993 A concurrent, generationnal garbage collector for a multithreaded implementation of ML qui était resté lettre morte avant de servir de base au projet OCaml-multicore. Comme pour pijul, cela pose pas mal de problèmes théoriques qui doivent d'abord être pleinement résolus avant d'avoir plus qu'un prototype. Le projet avance, mais au rythme de la recherche… ;-)

Même les téléphones portables ont des tas de cœurs, et la communauté OCaml est encore en train d'expliquer à qui veut l'entendre que ce n'est pas la bonne façon de programmer.

J'avais donc vu juste au niveau des besoins de parallélisation ? Je dois reconnaître que j'ai aussi du mal à comprendre la réaction d'une partie de la communauté quand elle explique que ce n'est pas la bonne façon de programmer.

Il y a bien des bibliothèques pour le parallélisme, comme functory, mais elles profiteraient d'un GC adapté au multi-cœur. Je m'étais servi de cette dernière pour faire le test du benchmark game sur les GC et ça rivalisait avec Rust (mais j'ai dû tuner le GC pour arriver à égaler les performances en temps CPU et c'était coûteux en mémoire).

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

C'est clair que ce sont les bugs les plus difficiles à dénicher et que Rust fournit un moyen de minimiser les risques mais je trouve quand même la mécanique super lourde.

Alors rejoins le mouvement des Insoumis et prône l'abolition de la concurrence, ainsi que de la défense de la propriété privée poussée à l'extrême en Rust. Mais je sens qu'un riche milliardaire profitant des innovations technologiques de la firme créée par son père n'est pas prêt à franchir le pas ! :-P

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

loin de moi l'idée d'ouvrir une guerre de paroisses

D'un autre côté, il a déjà du faire face à des commentateurs défendant git, il craignait peut être que ce soit pareil ici (d'autant que les guerres de chapelle entre langage peuvent être âpres).

Qu'est-ce qui ne vas pas avec les threads?

Le parallélisme ? Les approches à la Lwt (ou Async) c'est pratique mais ça ne parallélise pas les calculs sur tous les core du CPU. J'ai l'impression que la propriété de commutativité entre patchs indépendants se prête bien à la parallélisation des calculs. Il y a bien le projet ocaml-multicore (encore chez OCaml Labs) à base de fibres mais il en est encore au stade de la recherche (bien qu'il avance sûrement).

À l'heure actuelle, il faut forker (comme dans cet exemple du benchmark game) pour faire du map-reduce en parallèle, ce qui n'est pas des plus adapté comme solution.

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

je considère un peu rapidement que les sommets d'un graphe et ses arêtes sont des ensembles

Disons que la notion d'ensembles en mathématique est ambigüe (cf. le pardoxe de Russel), alors j'ai tendance à utiliser ce terme pour désigner les objets d'un modèle de la théorie des ensembles (ou les sommets d'un graphe qui est modèle de la théorie). Ce qu'il y a avec ZF (comme avec la théorie des catégories) est que l'on peut réflchir la métathéorie dans la théorie elle-même et aboutir à des théorèmes du style : si ZF est consistante alors elle a un modèle dénombrable (bien que le modèle en question possède des ensembles non dénombrables de son point de vue).

Pour une présentation succincte de la théorie des catégories, il y a le cours Inititation à la théorie des catégories de Gérad Huet qui commence ainsi :

Une catégorie C se compose d'objets et de flèches. On écrit A : C pour dire que A est un objet de C, et f : C(A,B) pour dire que f est une flèche de C reliant l'objet A à l'objet B. En général la catégorie dans laquelle on travail est sous-entendue, et on écrit plus simplement f : A -> B.

Jusqu'ici, une catégorie est un graphe orienté dont les nœuds sont les objets et les arcs sont les flèches. Mais les catégories possèdent la structure minimale donnée par l'associativité de la composition des flèches. Les flèches doivent donc être vue comme les chemins du graphe, quotientés par l'égalité des flèches.

Comme les notations ci-dessus te rappellerons celles utilisées pour les annotations de typage en OCaml, et que CAML signifie Categorical Abstract Machine Language (c'est la machine abstraite du bytecode OCaml), tu pourras aussi jeter un œil à De la déduction naturelle a la machine categorique :

Le titre de cet article résume trois slogans :

• La Déduction naturelle, c'est du lambda-calcul.
• Le lambda-calcul, c'est la théorie des Catégories Cartésiennes Fermées.
• La théorie des Catégories Cartésiennes Fermées, c'est du langage machine.

On réalise ainsi le Programme de Constructivation des Mathématiques :

   preuve       ---->  programme   ---->  combinateur --->    code
intuitionniste         fonctionnel        catégorique       exécutable

Sinon, pour en revenir à pijul, j'ai eu une nouvelle idée pour présenter la notion de fusion dans ce système. Quand on a une relation reflexive et transitive (un préodre), on peut la voir comme une catégorie (en réalité ce sont les catégories ayant au plus une flèche entre deux objets). Prenons, par exemple, la catégorie dont les objets sont les entiers et la relation de préodre « être un multiple de ». Ainsi le schéma de fusion suivant :

peut se lire : A et B sont des mutliples de O (A = p * O et B = q * O) et M (M = r * A = s * B) est un multiple commun de A et B. Mais parmi tous les mutliples communs de A et B, il y en a un qui est plus petit que les autres : c'est lui la fusion !!! Ce qu'exprime ce diagramme :

si je prends un autre multiple F de A et B alors il est multiple de leur ppcm M.

Cette notion, qui est une généralisation de la notion de borne supérieure (le plus petit des majorants si on y voit une relation d'ordre, le descendant minimal dans l'historique du dépôt) est ce que les catégoriciens appellent une somme amalgamée. Comme une telle somme n'existe pas toujours si on prend pour objets des fichiers, il faut prendre pour objets des digles.

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

Il me semble que le principal inconvénient, à l'époque, d'OCaml comme choix a été le support sur Windows.

Et il semble bien qu'un bon support de Windows soit un critère essentiel pour pijul, ils ont même écrit leur propre bibliothèque ssh pour cela (openssh supporte mal Windows). Il y a peut être aussi des raisons liées à la performance, en particulier sur la gestion du parallélisme (les quelques libs que j'ai testées pour faire du map-reduce sont tout de même coûteuses en mémoire, ocaml-multicore devrait résoudre ce problème).

Le mieux serait que pmeunier expose ses raisons, mais il est peut être passé à côté de la question.

Mais bon, si j'ai le temps je pourrais m'y pencher et faire revivre l'implémentation en OCaml :D !

Implémenter git en OCaml ne t'a pas suffit ! ;-D Tu vas devenir un spécialiste des systèmes de gestion de versions.

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

Ce n'est pas plutôt le contraire?

Non, c'est bien ce que j'ai écrit : toute catégorie est un graphe orienté, mais la réciproque est fausse. Une catégorie est un graphe orienté qui doit vérifier un certain nombre d'axiomes; autrement dit, ces axiomes sont des contraintes imposées au graphe et tout graphe qui ne les satisfait pas ne peut représenter une catégorie.

Comme tu évoques la notion d'ensemble, voici un exemple : un modèle de la théorie des ensembles est un graphe orienté qui n'est pas une catégorie. La théorie des ensembles est une théorie axiomatique d'une relation binaire que l'on appelle l'appartenance (notée ) et une relation binaire peut parfaitement se représenter comme un graphe orienté où l'existence d'une relation entre deux objets est signifiée par la présence d'une arête entre les deux sommets du graphe. Pour qu'un tel graphe puisse représenté une catégorie, il faudrait que la relation soit réflexive et transitive : ce qui n'est pas le cas de la relation d'appartenance, ni de nombreuses autres relations binaires.

En revanche on peut toujours, à partir d'un graphe orienté, engendrer une catégorie en prenant sa fermeture transitive :

puis en rajoutant une flèche de chaque sommet vers lui-même.

Pour revenir sur le graphe de l'univers des ensembles, les contraintes imposées par les axiomes sont tels que l'on peut plonger ou encoder n'importe quelle construction mathématique en son sein. La généralité de la notion de catégorie permet de faire la même chose : ce sont deux approches distinctes sur le fondement des mathématiques mais d'égale utilité.

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

C'est marrant comme il suffit de parler d'un concept mathématique relativement avancé en termes un tant soit peu profanes pour t'invoquer.

Je n'ai pas vu à quel moment il a été fait mention d'un concept mathématique relativement avancé en termes profanes. Tu disais que git gère un graphe orienté d'états successifs, je t'ai répondu que pijul faisait de même.

Je sais d'avance que la suite de cette conversation sera, en réponse, un autre pavé encore plus indigeste pour moi, que je ne comprendrai carrément pas, car j'ai arrêté les maths suffisamment tôt pour ma satisfaction professionnelle vu que j'aime mon travail, mais trop tôt par rapport à la maitrise d'icelles que j'aimerais avoir, mais bon je me lance quand même.

Si mes réponse apparaissent comme des pavés indigestes, alors c'est que j'ai échoué à atteindre mon objectif. Mon intention principale, quand j'écris sur ce site, est d'être compris par le plus grand nombre et non d'utiliser des termes pédants et abscons. Ton choix d'avoir arrêté les maths suffisamment tôt pour ta satisfaction professionnelle est on ne peut plus respectable : chacun fait et étudie ce qu'il lui plait. Cela étant, si je peux réussir à te faire comprendre ce qui distingue git et pijul sans entrer dans des détails techniques et théoriques, j'aurai atteint mon objectif.

Du peu que je sais j'ai l'impression que le c'est-à-dire est à l'envers.

Comme te l'a déjà répondu Michaël : toute catégorie peut être vu comme un graphe orienté (on les présente souvent ainsi d'ailleurs) mais la réciproque n'est pas vraie; mon c'est-à-dire n'est pas mis à l'envers. Mais laissons donc de côté le concept de catégorie et gardons donc celui de graphe orienté : il sera compris de tout le monde.

Git stocke en premier lieu des "états"-"sommets" qui représentent concrètement et trivialement le contenu brut du dépôt aux instants T(x), et ajoute par dessus un graphe de relations bête et méchant. J'ai l'impression que pijul travaille dans l'autre sens en ayant comme citoyen de première classe les arêtes avec le patch comme contenu, et en déduit des sommets-"état du dépôt".

De ce que j'en ai lu et compris, pijul aussi a pour sommets dans son graphe le contenu du dépôt aux instants T(x), à savoir les fichiers de la branche de travail. En revanche, pijul voit l'évolution de l'historique d'un dépôt comme un succession de patchs appliqués sur lui et c'est ce que représente son graphe en étiquetant chaque arêtes par un patch. Ce qui donne bien aux patchs un statut de citoyens de première classe, mais il ne passe pas son temps à déduire les fichiers par application des patchs par simple soucis d'efficacité :

Fast algorithms: Pijul's pristine can be seen as a "cache" of applied patches, to which new patches can be applied directly, without having to compute anything on the repository's history.

pijul documentation

Venons-en maintenant à une propriété qui distingue git et pijul : l'associativité. C'est certes une notion mathématique mais simple à comprendre : elle dit, en gros, dans le cas de l'addition, que (a + b) + c = a + (b + c) ce qui fait qu'en général on se dispense d'écrire les parenthèses et que l'on écrit tout simplement a + b + c.

Il est très utile, en pratique, d'avoir des opérations associatives et lorsque ce n'est pas le cas, il faut faire attention à la manière dont on les regroupe. Si je reprend l'exemple de la multiplication des matrices données dans un autre journal pour réduire le nombre de cache miss :

/* traduction directe de la formule du produit */
for (i = 0; i < N; ++i)
  for (j = 0; j < N; ++j)
    for (k = 0; k < N; ++k)
      res[i][j] += mul1[i][k] * mul2[k][j];

/* optimisation pour réduire les cache miss */
for (i = 0; i < N; i += SM)
  for (j = 0; j < N; j += SM)
    for (k = 0; k < N; k += SM)
      for (i2 = 0, rres = &res[i][j],
           rmul1 = &mul1[i][k]; i2 < SM;
           ++i2, rres += N, rmul1 += N)
        for (k2 = 0, rmul2 = &mul2[k][j];
             k2 < SM; ++k2, rmul2 += N)
          for (j2 = 0; j2 < SM; ++j2)
            rres[j2] += rmul1[k2] * rmul2[j2];

Dans son article, Ulrich Drepper précise bien « we ignore arithmetic effects here which might change the occurrence of overflows, underflows, or rounding », et il a raison : l'addition n'étant pas associative en arithmétique flottante, les deux programmes ne sont pas identiques. Mais son intention était surtout de montrer que l'ordre dans lequel les instructions étaient effectuées avaient son importance sur la gestion du cache CPU.

Quittons cette courte digression et revenons à nos moutons. Si l'arithmétique flottante n'est pas associative, il n'en est pas de même des séries d'instructions dans un langage comme le C : (e1;e2);e3 se comporte comme e1;(e2;e3) ou e1;e2;e3. Par contre, la fusion des patchs et commits en git ne vérifient pas cette propriété. C'est ce qui lui est reproché, entre autre, par les promoteurs de darcs et pijul. Le lien du premier commentaire illustrait ce phénomène, et la documentation de pijul l'illustre avec ces deux schémas :

si chaque point illustre des patchs appliqués, disons A B C, alors avec git on aurait : (A;B);C ≠ A;(B;C). C'est ce qui se passe quand on fait du cherry-picking et du rebase. En revanche, pijul vérifie bien cela et c'est ce qu'illustrait ce graphe :

Si l'on part de l'état O du dépôt, qu'Alice et Bob fork pour aller l'un dans l'état B et l'autre dans l'état C. Puis Alice passe ensuite dans l'état M. Peu importe que l'on fusionne d'abord B et C dans l'état N pour ensuite fusionner N et M, ou que l'on fusionne directement C et M : dans tous les cas on arrivera sur le même état Q. Pour revenir rapidement sur la notion de catégorie, cette propriété d'associativité fait partie de sa définition : un graphe qui ne la vérifie pas ne peut être vu comme une catégorie, en revanche une catégorie vue comme un graphe la vérifiera.

Comme l'a dit pmeunier, git ne vérifiant pas cette propriété (pourtant utile et, dans le fond, désirée par les utilisateurs), il y a des guides de bonnes pratiques pour combler cette lacune, là où, par construction, elle est automatiquement satisfaite dans pijul.

Outre cette propriété d'associativité des patchs, il y en a une autre fort utile : celle qui cherche à capter l'essence de fonctionnalités orthogonales ou indépendantes. Si, dans un commit, je modifie une partie d'un fichier, puis dans le commit suivant j'en modifie une autre qui n'a rien à voir : peu importe l'ordre dans lequel je les réalise, on devrait aboutir au même résultat. Cette propriété s'appelle la commutativité des patchs, à savoir p1;p2 fait la même chose que p2;p1 (ou a + b = b + a). Pijul détecte automatiquement de telle situation et transforme (de manière transparente pour l'utilisateur) le graphe de dépendance des états. Dans une telle situation :

pijul va chercher s'il ne peut trouver un patchs a(q) telle que dans le graphe suivant :

la fusion des états A et C donne le même état B que dans la séquence p;q, et en arrière plan on aura dans le graphe de pijul cette situation :

ce qui permet, entre autre, de paralléliser les calculs, mais rend aussi le graphe plus flexible à l'usage. Les guides de bonnes pratiques expliquent également comment obtenir une telle chose en git : avec pijul, rien à faire, elle est fournie de base sans effort de le part des utilisateurs.

Un dernier point, un peu plus technique que ce qui précède, mais pas si difficile à comprendre, c'est là raison d'être des digle. Lorsque l'on cherche à fusionner deux états, on se retrouve dans la situation suivante :

     A
   /   \
  /     \
O        ??
  \     /
   \   /
     B

Le problème est que si l'on prend pour type des sommets celui des fichiers, ce problème n'a pas toujours de solution : c'est ce qu'il se passe lorsqu'il y a conflit. Il y a un principe général qui consiste à dire : si le problème n'a pas de solution, alors agrandissons l'espace du possible et il aura toujours une solution. C'est, pour donner une comparaison, ce qu'on fait les algébristes quand ils ont inventé les nombres complexes : certains polynômes n'ont pas de racines, ce n'est pas grave, il suffit de rajouter des nombres et tout polynôme aura une racine. Raison pour laquelle, en cas de conflit, pijul produit pour sommet un graphe orienté de lignes et non un fichier. De la même façon que l'on peut projeter de plusieurs façons différentes un nombre complexe sur un nombre réel, on peut aplatir de différentes façon un digle en un fichier ou réduire de différentes façons un conflit. Mais cette phase ne résolution, comme dans git, n'est pas effectuée automatiquement par pijul mais reste à la charge des programmeurs.

En espérant avoir éclairci quelques différences entre git et pijul, sans avoir écrit un pavet indigeste.

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

Au delà de l'aspect esthétique – dont l'expérience montre en général qu'un problème mieux représenté est également mieux compris et les traitements afférents sont plus faciles –

Au fond, je n'en doute pas vraiment. J'ai présenté la chose ainsi¹ pour ne pas heurter certaines sensibilités. Si je devait faire un parallèle, le fondement du système me fait penser au passage du paradigme ptoléméen avec ces épicycles au paradigme héliocentrique de Copernic et Kepler.

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

Qu'est-ce que pijul va faire au merge ?

Il va dire qu'il y a conflit, comme git. Mais la différence entre les deux outils (ou plutôt entre leur fondement théorique) ne se situe pas à ce niveau là, c'est-à-dire que ce n'est pas sur ce genre de question qu'ils se distinguent : pijul n'est en rien un outil magique qui résout tout seul les conflits de merge en devinant ce qu'il y a dans la tête des programmeurs.

En fait, je me suis rendu compte que j'ai mal utilisé le terme de « 3-way merge » ce qui t'a sans doute induit en erreur sur le fonctionnement de pijul.

Je n'ai pas le temps de corriger mon erreur de présentation, j'essaierai de voir demain. Sinon, le plus simple est d'aller lire les deux articles de blog que j'ai donné en lien, je voulais juste en faire un résumé et un teaser.

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

Je m'avance beaucoup sur la maitrise de la chose, mais git ne gère pas des patchs mais un graphe orienté d'états successifs.

pijul aussi gère, à sa façon, un graphe orienté d'états successifs : un dépôt c'est une catégorie, c'est-à-dire un graphe orienté qui vérifie certaines propriétés. Les sommets du graphes sont des « fichiers » et les arcs des patchs : si il y a un arcs entre deux sommets alors la cible est le résultat du patch appliqué à la source.

En réalité les sommets ne sont pas des fichiers mais une notion étendue des ceux-ci : des digle (directed graph fi le). Si le graphe est linéaire on a un fichier au sens usuel (ligne à ligne), tandis que l'on obtient un graphe en cas de conflit lors d'un merge.

Résoudre un conflit revient juste à appliquer un patch sur un tel sommet : ainsi pijul garde en mémoire, dans son graphe, le sommet conflictuel au lien de l'effacer.

Un des propriétés marrantes c'est l'associativité des patchs :

Ici on a un 3-way merge¹ qui s'obtient naturellement comme la composition de merge de 2 patchs : quelque soit le chemin pris on arrivera toujours sur le même état final Q. C'est cette propriété que n'ont pas les autres DCVS comme git et qui constitue la reproche des partisans de darcs et pijul.

Après, je ne sais pas si en pratique cela s'avérera d'un grand intérêt et plus souple à l'usage que l'existant, mais la théorie qu'il y a derrière est jolie. Elle est expliquée plus en détail dans ces deux articles de blogs :

• Merging and patches
• Merging, patches, and pijul

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

Bah non ça va plus vite : si tu mets moins de temps pour faire la même chose (O.76 seconde au lieu de 1 seconde), tu vas plus vite. Il a réduit le temps d'exécution de 24% et donc augmenté la vitesse de 31% (1 / 0.76 ~ 1.31).

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

Je me disais que passais à côté de la blague.

Pour calmer des chiens de garde, il faut leur caresser l'échine ? :-P

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

L'exemple avait pour but d'illustrer l'analogie et la correspondance fonctionnelle entre un théorème et un programme, ainsi que le parallèle entre la recherche de preuve et la résolution algorithmique d'un problème. On ne peut nullement en conclure :

• que toute fonction ainsi obtenue est efficace (complexité tant en temps qu'en espace) ;
• que toute fonction ainsi obtenue est inefficace.

Je n'ai jamais soutenu la première (ce que tu laisses sous-entendre), tu sembles fortement insister pour soutenir la seconde. Les deux propositions n'étant pas antinomiques, il reste une troisième possibilité…

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

Je crois qu'il y a un problème de compréhension entre nous.

Non c'est ton interprétation biaisé. L'informatique n'est en rien une branche des mathématiques, sauf dans l'esprit tordu des logiciens qui ne peuvent la concevoir autrement.

C'est exactement ce que je venais d'écrire et je suis d'accord avec toi, m'étais-je mal exprimé ? Ma phrase que tu cites était :

autrement elles ne seraient pas traitée comme deux sciences distinctes, mais la première serait simplement une branche de la seconde.

Que l'on pourrait reformuler ainsi : si l'informatique était une branche des mathématiques alors elles ne seraient pas traitées comme deux sciences distinctes, or elles sont traitées comme deux sciences distinctes (à bon droit), donc l'informatique n'est en rien une branche des mathématiques.

Je ne vois pas comment je peux exprimer plus clairement le fond de ma pensée. À quel moment ai-j écrit (ou peut-on conclure de mes commentaires) que l'informatique est une branche des mathématiques ?

Ah manque d'arguments donc attaque personnelle.

Ce n'était nullement une attaque personnelle. La photo est une caricature grossière : n'importe quelle personne, même quelqu'un n'ayant jamais étudié la physique, comprend que l'équilibre de gauche est totalement instable. C'est en cela qu'il me fait plus penser à la solution proposée par freem à laquelle GuieA_7 reprochée (je le cite) :

À part des cas très spécifiques, par exemple toutes ces conditions sont vérifiées:

• on n'a pas de thread donc pas possible que ça introduise un bug.
• on a vérifié que l'optimisation règle effectivement un problème en production très critique.
• on doit livrer très rapidement une version qui corrige ledit problème mais sans casser l'API, et derrière on fera une version avec une nouvelle API correcte (celle que je proposait par exemple) (on peut même garder la vieille API en "deprecated").

soit on garde la vielle version (lente mais correcte), soit on fait une version rapide et correcte (ce qui en l'occurrence n'était pas bien long, les lignes en plus n'étant quelques déclarations). Mais conseiller en premier une bidouille infâme ne me semble pas une bonne chose ; le C++ est déjà assez piégeux comme ça.

réponse (d'un ingénieur ou d'un scientifique, peu m'importe je ne suis ni l'un ni l'autre, je ne suis dans aucun camp et n'est pas de problème d'égo) qui relève clairement du côté droit de ton image.

Donc l'informatique tout entière peut-être ramenée à un système de typage et un triangle rectangle. Intéressant comme la logique d'un logicien peut parfois être biaisé quand ça l'arrange.

Je n'ai jamais soutenu une telle chose.

Ton pavé ne change strictement rien à ce que je disais.

Tel n'était pas son but. Il avait pour finalité d'apporter une objection à ce propos : « l'idée d'adopter une pensée mathématique quand on code¹ ne me semble pas une bonne idée du tout » et de montrer qu'une pensée structurée mathématiquement² pouvait traiter les problématiques attendues par arnaudus, à savoir : « efficacité de l'algorithme en temps et en mémoire, gestion des arrondis, évolutivité, modularité et clarté du code ».

re-déballe en boucle ses propres examples non corrélés.

Qu'entends-tu pas exemples non corrélés ? Les lignes automatiques du métro parisien (la ligne 14 date de la fin des années 90) est-ce un exemple corrélé et qui te conviendrait ?

L'inventeur de l'atelier B a donné une conférence sur le sujet au Collège de France. Il se présente ainsi :

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.

Au sujet du développement de la ligne 14, il y dit :

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 pour méthode de développement :

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

J'ai du mal à croire qu'un tel système n'est pas à gérer du threading et des I/O.

Du côté de Coq, j'ai du mal à voir CompertCert (un compilateur C certifié) comme un échec des approches formelles. Xavier Leroy a même reçu le prix Milner, entre autre pour cela, et j'avais écrit un journal à l'occasion.

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

Petit ajout, pour reprendre ton image :

L'image de gauche c'est freem rappeler à l'ordre par GuieA_7, l'image de droite c'est ce que je prônes; mais bizarrement j'inverserais les légendes. :-P

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

Je vais me faire l'avocat du diable mais allons y…

Objection rejetée ! :-P

Non que je sois en désaccord avec ce que tu dis, mais tu as mal interprété mes propos (peut être bien par ma faute, je me suis sans doute mal exprimé). Je n'ai jamais dit cela :

Réduire l'informatique aux Maths et à la preuve formelle uniquement est une stupidité.

autrement elles ne seraient pas traitée comme deux sciences distinctes, mais la première serait simplement une branche de la seconde. Néanmoins quand je regarde l'image de ton message, la première impression qui me vient à l'esprit est celle-ci : elle a été faite par un ingénieur, autrement dit une personne qui se fait une fausse idée de ce qu'est la science mais qui veut tout de même exprimer son avis dessus.

Il n'en reste pas moins que les mathématiques et la preuve formelle fournissent les outils conceptuels, par exemple, pour les systèmes de typage langage de programmation. Je reprends mon exemple de Pythagore : si en entrée tui lui donnes un carré, il va te répondre qu'elle n'a pas le bon type, lui il veut un triangle rectangle ! Par contre, tu as un autre théorème qui te dis que si tu coupes un carré selon sa diagonale, tu obtiens deux triangles rectangles. Et boum, en composant les deux théorèmes, tu résous le problème de la duplication du carré : à partir d'un carré donné, construire un carré de surface double. La démarche est strictement similaire, dans l'organisation du discours, à ce que l'on fait en programmation en découpant le code en fonctions que l'on combine ensemble. D'un problème compliqué, on le découpe en problème plus simple, et on obtient la solution par composition : divide and conquer. On obtient alors ce parallèle entre informatique et mathématique :

Informatique	Mathématiques
Type	Formule
Programme	Preuve
Primitive système	Axiome
Fonction de A vers B	Preuve de « A implique B »
Paire de A et B	Preuve de « A et B »
Type somme sur A et B	Preuve de « A ou B »
Interpréteur	Théorème de correction
Décompilateur	Théorème de complétude

J'ai repris le tableau de la dépêche de Perthmâd sur Coq 8.5, tu pourras t'y reporter pour de plus amples développements.

Je régissais au départ à cette proposition d'arnaudus :

Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout.

Les liens sont tout sauf ténus, soutenir le contraire est une ineptie. Mais reprenons un exigence d'arnaudus :

(efficacité de l'algorithme en temps et en mémoire, gestion des arrondis, évolutivité, modularité et clarté du code)

La pensée mathématique ne serait-elle pas totalement modulaire, par exemple ? Le travail des algébristes, par exemple, qui classent leurs structures en monoïdes, groupes, groupes abéliens, anneaux, corps, espaces vectoriels… Et en algèbre linéaire, pour reprendre le calcul sur matrices, les théories parlent d'espaces vectoriels sur un corps quelconques (le corps des réels n'étant qu'un corps particuliers), les théorèmes et preuves sont faites sur un corps des scalaires quelconques : la voilà la programmation générique et la modularité ! On voit la route s'ouvrir vers le polymorphisme paramétrique, i.e. les types paramétrés, les templates du C++, les generics du Java et j'en passe (voir le besoin exprimé par l'échange entre Gabbro et Albert_ plus bas dans le fil de discussion).

Illustration avec le concept le plus simple : le monoïde. C'est une structure munie d'une opération interne et d'un élément neutre pour celle-ci (comme les entiers avec l'addition).

module type Monoid = sig
  type t
  val e : t
  val op : t -> t -> t
end

À partir de là, on peut facilement, sur un monoïde donné, répéter l'application de l'opérateur interne sur une suite d'élément, comme lorsque l'on calcule la somme 1 + 2 + 3 + 4.

let sum (type a) (module M : Monoid with type t = a) =
  List.fold_left M.op M.e

Maintenant, outre les entiers munis de l'addition avec 0 pour élément neutre, on peut remarquer que les string muni de l'opération de concaténation forme un monoïde avec pour élément neutre la chaîne vide "".

module String_mon = struct
  type t = string
  let e = ""
  let op = ( ^ )
end

On peut faire pareil avec les int et l'addition, les int et la multiplication, ou bien encore les listes et l'opération de concaténation.

module Int_plus_mon = struct
  type t = int
  let e = 0
  let op = ( + )
end

module Int_mul_mon = struct
  type t = int
  let e = 1
  let op = ( * )
end

module List_mon (T : sig type t end) : Monoid with type t = T.t list = struct
  type t = T.t list
  let e = []
  let op = ( @ )
end

Voyons voir à l'usage :

sum (module Int_plus_mon) [1; 2; 3; 4];;
- : int = 10

sum (module Int_mul_mon) [1; 2; 3; 4];;
- : int = 24

sum (module String_mon) ["Hello"; " "; "World!"];;
- : string = "Hello World!"

sum (module List_mon(struct type t = int end)) [[1; 2]; [3; 4]];;
- : int list = [1; 2; 3; 4]

Et là je définis le produit scalaire comme en Python dans mon commentaire précédent, mais avec la garantie du typage statique (le type checker vérifie que ma preuve n'a pas de vice de forme) :

let dotprod v1 v2 = sum (module Int_plus_mon) (List.map2 ( * ) v1 v2);;
val dotprod : int list -> int list -> int = <fun>

dotprod [1; 2; 3] [3; 4; 5];;
- : int = 26

On peut aller plus loin, là c'était un simple échauffement. :-) L'exemple vient d'une bibliothèque dont l'annonce de publication a été faite hier sur le forum OCaml. Prenons un algorithme qui a cet forme :

algorithm a b ::=
         x := f a;
         y := f b;
         return (x + y);

où f est une fonction définie ailleurs dans le code. On pourrait aller plus loin puis le paramétrer par la fonction f et la fonction appliquée sur x et y avant d'être retournée.

 algorithm ((_ + _), (f _)) a b ::=
         x := f a;
         y := f b;
         return (x + y);

Ici le return et le point-virgule ; ont usuellement une sémantique bien définie par le langage : ce couple forme ce que l'on appelle une monade (là je sens les haskelleux venir en masse). On peut donc paramétrer l'algorithme par une monade et prendre de la liberté vis à vis d'une sémantique contrainte par le langage hôte :

algorithm ((return _), (_ := _ ; _)) ((_ + _), (f _)) a b ::=
         x := f a;
         y := f b;
         return (x + y);

le paramètre (_ := _ ; _), qui contrôle la sémantique du ;, est usuellement appelé bind. Ce qui donne la signature de module suivante :

module type Monad = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
end

et notre algorithme devient un module paramétré par une monade et un autre module qui contient les interprétations de + et f.

module Algorithm (M : Monad) (R : ... ) = struct
   open R
   open M

   let run a b =
     f a >>= fun x ->
     f b >>= fun y ->
     return (x + y)
end

ici >>= est un alias courant pour bind quand on joue avec les monades, et run sert comme son nom l'indique à exécuter le calcul. Il existe un paquet de monades intéressantes (en plus de celle avec le sens usuel de ; et return dans les langages impératifs), la documentation de la bibliothèque en question en donne quelques exemples (bibliothèque à la structure on ne peut plus modulaire). Et tout cela sert bien évidemment à produire des logiciels, en l'occurence le projet BAP (Binary Analysis Platform) :

The Binary Analysis Platform is a reverse engineering and program analysis platform that targets binaries, i.e., compiled programs without the source code. BAP supports multiple architectures (more than 30), though the first tier architectures are x86, x86-64, and ARM. BAP operates by disassembling and lifting the binary code into the RISC-like BAP Instruction Language (BIL). Thus the analysis, implemented in BAP, is architecture independent in a sense that it will work equally well for all the supported architectures. The platform comes with a set of tools, libraries, and plugins. The main purpose of BAP is to provide a toolkit for automated program analysis. BAP is written in OCaml and it is the preferred language to write analysis, we have bindings to C, Python and Rust.

Quand je regarde l'architecture de cette bibliothèque, la dernière pensée qui me vient à l'esprit est bien celle-ci : « l'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout », mais au contraire je me dis : l'idée d'adopter une pensée mathématique quand on code me semble une excellente idée ! :-)

On veut un truc qui marche rapidement : on va au plus simple; on veut plus de sécurité : on adapte la monade; on veut travailler sur l'optimisation : on change le module de l'algorithme… Vous ne voyez toujours pas l'utilité ? Alors effectivement, toutes ces contraintes auxquels il faut s'adapter proviennent du monde extérieur et donc sont en quelques sortes extra-mathématiques, mais croire que la méthodologie mathématique est inadaptée, voire impropre, au besoin de l'ingénieur informaticien c'est ignorer ce que sont les mathématiques.

Et pour terminer sur ces histoires d'optimisation de code (et donc de compléxité algorithmique), je citerai la présentation du module Logique et théorie du calcul du MDFI :

La théorie de la calculabilité s'intéresse essentiellement à la question suivante : au moyen d'un ordinateur, quelles fonctions peut-on calculer et quels problèmes peut-on résoudre ? Son développement est concomitant de l'apparition des principaux modèles de calcul (fonctions récursives, machines de Turing, lambda-calcul,…) et est très étroitement lié à la logique mathématique : théorème d'incomplétude de Gödel (qui sera abordé dans ce cours), lambda-calcul typé (cours Preuves et types)…

La complexité cherche quant à elle à mesurer le degré de difficulté d'un problème, typiquement en termes de temps de calcul et d'espace utilisé. Il s'agit donc de questions plus fines, qui font l'objet de nombreuses recherches actuelles, notamment en rapport avec la logique.

L'objectif de ce cours est de présenter les outils et résultats fondamentaux pour aborder ces questions.

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

Tu détournes habilement le sujet, mais je pense que tu as tort sur le fond.

Je ne pense pas détourner le sujet, et je pense fondamentalement avoir raison sur le fond. ;-)

quand on code dans la plupart des langages (qui sont destinés à produire des logiciels et pas des démonstrations mathématiques), on doit avant tout penser aux aspects informatiques des problèmes (efficacité de l'algorithme en temps et en mémoire, gestion des arrondis, évolutivité, modularité et clarté du code). Dans ce cadre, les maths sont un outil, et pas un état d'esprit.

Et les concepts que tu mets en branle, dans ton esprit, quand tu penses aux aspects informatiques des problèmes, ils relèvent de quelle science à ton avis ? ;-) Je t'ai donné l'exemple d'une équipe membre de l'Institut de Recherche en Informatique Fondamentale qui s'associe avec une autre équipe de l'Institut Mathématique de Jussieu pour dispenser une formation intituler Logique Mathématique et Fondements de l'Informatique, et tu ne vois toujours pas le rapport ?

Tu me fais penser à M. Jourdain : il faisait de la prose sans le savoir mais, quand on lui a expliqué ce qu'était la prose, il a au moins reconnu qu'il en faisait. Toi c'est un peu différent, tu fais des mathématiques sans le savoir (sans doute par ce que tu ignores ce que sont les mathématiques et que tu n'en reconnais pas toujours quand tu en vois), je t'expliques qu'en réalité tu en fais quand tu programmes, mais tu restes dans le déni et prétends que tu n'en fais pas.

Je vais le dire autrement avec le théorème de Pythagore. Voilà un théorème qui dit : donne moi un triangle, je te construirais trois carrés dont la surface de l'un et la somme de la surface des autres. Autrement dit c'est une fonction qui prend en entrée un triangle et retourne un triplet de carré. Alors assurément, comme tout théorème, il a plus d'une démonstration mais elles font toutes la même chose. Cela étant, dans toutes ces démonstrations, il y en a qui sont plus efficaces que d'autres pour produire la sortie. C'est pareil pour toutes les fonctions que tu codes : ce sont des preuves de théorèmes mais certaines sont plus efficaces que d'autres. Que tu l'ignores ou que tu ne le vois pas, c'est une chose; que ce soit faux, s'en est une autre. ;-)

Pour revenir au débat d'origine avec aurelienpierre :

Mais je ne sais pas si tu as fait semblant de mal comprendre là où je voulais en venir, ou si je ne m'étais pas exprimé clairement. La question qu'on discutait, c'était de dire que la vectorisation était une manière intuitive en mathématique d'aborder un problème, et que les gens qui considéraient une boucle FOR plus intuitive qu'un calcul vectorisé avaient, en gros, un problème de formation.

Je ne sais pas trop ce qu'il faut entendre dans votre discussion par le terme vectorisation. S'agit-il des instructions SIMD des CPU ou de manipuler des structures de données abstraites représentant le concept mathématique de vecteur que l'on trouve en algèbre linéaire ?

Pour ce qui est des idiomes des langages, en python on utilisera volontiers des itérateurs plutôt que des boucles FOR (en C++ aussi, il me semble qu'il y a des itérateurs dans la STL). Le produit scalaire entre deux vecteurs se définira ainsi :

import operator
def dotprod(vec1, vec2):
  return sum(map(operator.mul, vec1, vec2))

et non avec une boucle FOR. Il me semble que c'était déjà, là, une des choses que voulait faire remarquer aurelienpierre. Dans un langage comme le C, assurément on fera la même chose avec une boucle FOR mais parce c'est là l'idiome du langage pour faire ce genre de calcul.

Revenons au calcul du produit matriciel et à la quette d'optimisation. En C, la traduction naïve de la chose donnerait :

for (i = 0; i < N; ++i)
    for (j = 0; j < N; ++j)
      for (k = 0; k < N; ++k)
        res[i][j] += mul1[i][k] * mul2[k][j];

Ici comme on parcourt la deuxième matrice colonne par colonne, sur de grosses matrices on a du cache miss. En la transposant d'abord on a :

double tmp[N][N];
  for (i = 0; i < N; ++i)
    for (j = 0; j < N; ++j)
      tmp[i][j] = mul2[j][i];
  for (i = 0; i < N; ++i)
    for (j = 0; j < N; ++j)
      for (k = 0; k < N; ++k)
        res[i][j] += mul1[i][k] * tmp[j][k];

Les exemples de code sont issus de Memory part 5: What programmers can do, une série d'articles sur LWN par Ulrich Drepper au sujet du fonctionnement de la mémoire et des caches. Rien que là, dans ses benchmarks, il a un gain de 76.6%.

Néanmoins, il faut allouer une matrice temporaire : c'est lourd et on a pas toujours l'envie ni la place de faire. Il propose alors mieux :

#define SM (CLS / sizeof (double))

  for (i = 0; i < N; i += SM)
      for (j = 0; j < N; j += SM)
          for (k = 0; k < N; k += SM)
              for (i2 = 0, rres = &res[i][j],
                   rmul1 = &mul1[i][k]; i2 < SM;
                   ++i2, rres += N, rmul1 += N)
                  for (k2 = 0, rmul2 = &mul2[k][j];
                       k2 < SM; ++k2, rmul2 += N)
                      for (j2 = 0; j2 < SM; ++j2)
                          rres[j2] += rmul1[k2] * rmul2[j2];

et il compile le code avec gcc -DCLS=$(getconf LEVEL1_DCACHE_LINESIZE) pour optimiser le code pour la machine sur lequel il est compilé : CLS représente la taille d'une ligne de cache de niveau 1 sur la machine. Et là ce qu'il fait, avec des boucles FOR parce que tel est l'idome du C, c'est suivre la courbe en Z de Lebesgue (cf. mon premier commentaire) en adaptant la taille des zigzag à celui de la ligne de cache.

Il évite ainsi d'allouer une matrice temporaire pour calculer la transposer et il gagne 6.1% de plus qu'avec le code précédent. Mais au fond ce qu'il vient d'écrire ce n'est que la traduction dans le langage formel qu'est le C d'une pensée qui est mathématique de part en part.

Il conclue, enfin, en disant que l'on peut aller encore plus loin en vectorisant (instruction SIMD) le code et gagner encore 7.3%. À l'arrivée, il a un code qui va 10% plus vite que la boucle FOR naïve.

Ceci étant, les compilateurs appliquent déjà des optimisations de ce genre (pas forcément sur ces problèmes, mais sur d'autres) mais pour ce faire leurs auteurs, eux, connaissent l'outillage conceptuel mathématique nécessaire et il vaut mieux les laisser faire que d'essayer de le faire soi-même (ce que tu as reconnu ;-).

Encore un autre exemple, si tu n'est toujours pas convaincu. Voici une liste chaînée :

: -> : -> : -> : -> []
|    |    |    |
1    2    3    4

elle a sa petite sœur, la liste doublement chaînée :

] <- : <- : <- FOCUS -> : -> []
      |    |      |      |
      1    2      3      4

en programmation fonctionnelle on appelle cela le zipper sur une liste. Et bien le zipper (ou liste doublement chaînée) et le type dérivé du type des listes chaînées. Explication ici : The algebra (and calculus!) of algebraic data types, on tu verras du développement en série entières et du calcul différentiel sur des types. ;-)

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

Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout.

J'imagine, comme GuieA_7, que c'est de l'humour, mais vu l'incubateur d'excellence qu'est LinuxFr, je vais quand même répondre. :)

En mathématique, on a tout de même l'habitude d'apporter des preuves de ce que l'on affirme et non de lancer des affirmations en l'air. Tentons de réfuter le propos.

Déjà il me semble bien que Gödel, Church, Turing et Von Neumann étaient avant tout des mathématiciens et logiciens. J'ai là, sous les yeux, l'article de Turing où il expose son concept de machine et celui-ci est intitulé Théorie des nombres calculables, suivie d'une application au problème de la décision. Il traite ce fameux problème à la section 8 et montre son caractère insoluble : c'est le fameux problème de l'arrêt. Le problème en question fut posé par Hilbert et renvoie au deuxième des 23 qu'il posa au deuxième congrès international des mathématiciens, tenu à Paris en août 1900.

Ceci étant dit, on s'étonnera moins du fait que le laboratoire Preuves, Programmes, Systèmes (PPS) de l'Institut de Recherche en Informatique Fondamentale, associée à l'équipe de logique de l'Institut Mathématique de Jussieu, propose un master intitulé Logique Mathématique et Fondements de l'Informatique.

On s'étonnera moins, également, d'un résultat notoirement connu chez les théoriciens sous le nom de correspondance preuve-programme ou corresponcance de Curry-Howard : un programme est la preuve d'un théorème et l'énoncé de ce dernier est le type du programme. Dans cette lignée de pensée, on trouve le système F (ou lambda-calcul polymorphe) de Jean-Yves Girard qui est la base des langages (et de leur système de type) comme Haskell ou OCaml. Le système F date tout de même de 1972 et fut mis au point, entre autre, pour résoudre la conjecture de Takeuti qui généralise un résultat obtenu par Gentzen dans les années 30 afin de résoudre le fameux deuxième problème de Hilbert.

Illustration rapide avec le calcul de la longueur d'une liste chaînée :

let rec length = function
  | [] -> 0
  | _ :: tl -> 1 + length tl

let length_tr l =
  let rec loop acc = function
    | [] -> acc
    | _ :: tl -> loop (acc + 1) tl
  in loop 0 l

Déjà, on peut faire de la récursivité sans boucle for ni boucle while. La première version a un gros défaut : on risque le débordement de pile, la deuxième utilise un espace constant sur la pile (c'est l'équivalent d'une boucle for ou while). Mais les deux miment un principe de raisonnement standard en mathématique : le raisonnement par récurrence. Si une propriété est vraie de 0 (P 0), puis qu'elle passe au successeur (si Pn alors P(n+1)) alors elle est vraie pour tout entier (pour tout n, Pn). En réalité seule la deuxième utilise ce principe, la première utilise l'hypothèse de récurrence sous la forme : si pour tout m ≤ n, Pm alors P(n+1). Autrement dit, il faut garder sur la pile toutes les preuves depuis 0 pour passer à l'étape suivante : on risque le débordement de pile sur une machine. ;-)

Je pourrais continuer comme cela pendant longtemps mais, pour des langages comme le C, on pourra se reporter à l'excellent tutoriel Introduction à la preuve de programmes C avec Frama-C et son greffon WP sur le site zeste de savoir. Frama-C développé en partenariat par le CEA list et l'Inria.

Frama-C est une plateforme d’analyse de codes sources. Elle met en œuvre des techniques d’interprétation abstraite, de vérification déductive, de slicing et d’analyse dynamique dont la caractéristique commune est de reposer sur des méthodes formelles qui assurent que leurs résultats sont rigoureusement corrects. Dans une dynamique open-source, cette plateforme permet non seulement le développement d’approches variées par une communauté d’utilisateurs divers, mais aussi de combiner ces approches pour atteindre des objectifs de validation ambitieux. Ces analyses sont particulièrement adaptées à des programmes dans lesquels la sûreté de fonctionnement, ou la sécurité face aux actions malveillantes, est essentielle.

Pour conclure rapidement, sur les mathématiciens qui ne comprennent pas le problèmes de cache (ça, c'est pour freem). Voyons voir le calcul matriciel. Un matrice carré simple comme

1 2 3
4 5 6
7 8 9

est représentée en mémoire ligne par ligne 1 2 3 4 5 6 7 8 9 pour le C, ou colonne par colonne par 1 4 7 2 5 8 3 6 9 en Fortran. Résultat dans un langage comme le C si on parcourt une matrice ligne par ligne ça va plus vite et on a moins de cache miss sur de grosses matrices. Pour faire le produit, on peut par exemple transposer d'abord la seconde matrice avant de faire la boucle for qui calcule le produit pour avoir à parcourir les deux matrices ligne par ligne.

On peut aussi découper les matrices très grandes récursivement en matrice plus petite selon le procédé de la courbe de Lebesgue

comme cela on linéarise la représentation en mémoire de notre matrice en suivant la courbe et les petites matrices rentre bien sur une ligne de cache. Ensuite on fait du Map-Reduce pour opérer sur la grande matrice à partir des petites, ce qui en plus à l'avantage de bien se paralléliser.

On peut aussi utiliser, comme alternative, la courbe de Hilbert :

Pour les bases de données multi-dimensionnelles, la courbe de Hilbert a été proposée à la place de la courbe de Lebesgue parce qu'elle a un comportement préservant mieux la localité.

C'est joli et utile les fractales ! :-)

Alors toujours convaincu que : « Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout » ?

Ou je peux conclure comme un récent commentaire d'arnaudus :

En face de certains bistros, il y a des universités, et dans les universités, il y a des gens qui travaillent sérieusement sur de telles questions ; il existe par exemple des discipline scientifiques qui s'appellent Informatique et Mathématique et qui permettent d'aller un peu plus loin que les platitudes habituelles.

Désolé pour la conclusion, mais c'était de bonne guerre. ;-)

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

D'ailleurs je cherche encore une ressource accessible traitant de façon pertinente de l’implémentation de différentes structures de donnée (lazy ou non / mutable ou non) efficace sur des architectures de CPU modernes.

Je suppose que tu cherches des structures pour langage fonctionnel (comme dans le livre de Okasaki). Tu trouveras peut être ton bonheur dans ces liens :

• Cache efficient functionnal algorithms
• Vidéo de la conférence Functionally Oblivious and Succinct d'Edward Kmett
• Slides de la vidéo

Edward Kmett est l'auteur du blog The Comonad.Reader.

En espérant que ça puisse t'être utile.

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

Euh… tagless final ou GADT c'est bonnet blanc et blanc bonnet ! ;-)

Regarde bien dans mon article à la fin de la première partie. Les types des constructeurs de mon GADT sont justement ceux que je donne ensuite aux fonctions d'interprétations.

L'idée derrière la méthode tagless final est la même que celle exposée dans l'article EDSL et F-algèbres d'Aluminium95 à la différence que j'utilise des modules et non des enregistrements. Les modules sont justes des enregistrements extensibles (objets) dopés aux stéroïdes.

Après je dois avouer que je ne comprends pas trop les spécifications de ton langage, mais il faudra bien que tu écrives un type checker (qui est une interprétation comme une autre des termes du langage). De ce que je crois comprendre de ton intention, ça me fait penser aux typages des modules et foncteurs en OCaml, c'est pour cela que je les évoquaient. Mais je me trompe peut être là-dessus.

Par exemple, quand tu écris :

Ainsi, tu écris 'int ~ 1 ~ Name "a"', pour définir un truc du nom de "a" qui est de type int et vaux 1. Cela permet de le composer en plusieurs fois.

N'y a-t-il pas un rapport avec ce code ?

module M : sig
  type t
  val a : t
end = struct
  type t = int
  let a = 1
end

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

En réalité, la raison pour laquelle ce genre de «bug» ne peut pas arriver en C, ce n'est pas tant que le langage est «simple», mais parce que sa spécification est laxiste […]

Dans ces conditions, c'est plus effectivement facile pour un compilateur de respecter la spec' !

Ce n'est pas ce que dit l'article cité dans le commentaire auquel tu réponds : le problème se trouve dans la spécification du système de type de Java et non dans un compilateur donné. Le système de type de Java est unsound et cela d'après sa spécification.

L'exemple est celui-ci :

l'auteur de l'article précise bien qu'il y a des compilateurs qui refuseront de compiler en considérant qu'il y a une erreur de typage dans le code, mais alors le bug est dans le compilateur qui ne respecte pas la spécification du langage.

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