kantien a écrit 1187 commentaires

Cela dit si tu ne postules pas ça, il ne peux y avoir de sciences.

Les kantiens n'ont jamais nié une telle chose.

Je comprends pas trop en quoi tu postules que je veux me débarrasser de l’observateur.

Bah, quand on me dit que la pierre a une existence propre spatio-temporellement déterminée, j'interprète cela comme abstraction faite de tout rapport à un observateur possible, c'est-à-dire que l'on se débarrasse de l'observateur. Autrement dit, qu'il y est ou non des hommes, il existe un monde dans lequel des pierres évoluent dans l'espace et le temps et la physique est là pour découvrir les lois d'un tel monde. Ce que disent les kantiens, ce n'est rien d'autre que ce que disait Socrate : nous ne voyons que des ombres sur un mur, tels les esclaves de l'allégorie de la caverne. Qu'il y est quelque chose qui nous apparaisse comme une pierre spatio-temporellement déterminée, que cette chose soit bien réelle, nous l'accordons; nous disons juste qu'elle n'est telle que pour les êtres humains.

Je te répondrai plus en détail demain, mais j'ai l'impression que tu te méprends (comme Einstein lui-même d'ailleurs) sur ce que veulent dire les kantiens quand ils affirment que la pierre (ou tout autre objet physique) ne sont pas des choses en soi existant « sans nous ».

Donc « exécution » n’a pas trop de sens. Par contraste, en python, si tu passes un objet d’un mauvais type à une fonction, ben « boom ». Python se comportera pas bien du tout …

Disons que sans écrire un énoncé à quantificateur universelle borné (la condition ), on risque la contradiction ou l'énoncé vide de sens. ;-)

C’est une notion logique la notion de concept ?

Un peu mon neveux ! La logique s'occupe des règles pour former des concepts, des règles pour former des jugements à partir de ces concepts et des règles pour enchaîner ces jugements entre eux ou raisonnements. Le plan de la doctrine générale des éléments du traité sur la logique de Kant :

1. Des concepts
2. Des jugements
3. Des raisonnements

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

Le truc qui me choque à chaque fois que je croise ce genre de philosophie : et quand il y a 2 observateurs ? Et que par hasard ils sont d’accord, ce qui n’est pas systématique, mais assez commun. On peut donc arguer qu’ils tirent les mêmes conclusions sur l’objet en question, ce qui tend à montrer que ces phénomènes ont une existence propre.

Tu prends là une condition suffisante (l'existence propre de l'objet expliquerait l'accord des observateurs), pour une condition nécessaire (leur accord ne peut s'expliquer que par une existence propre de l'objet, abstraction faite du rapport à l'observateur).

Premièrement, l'accord entre observateurs sur les determinations spatio-temporelles des objets est tout sauf commun : voir les principes fondamentaux des relativité restreinte et générale. Deuxièmement, dans la connaissance expérimentale on ne pose jamais de questions sur ce que sont les choses en elles-même, mais seulement sur les résultats de nos observations; et parler d'observation sans observateur (c'est-à-dire en faisant abstraction du rapport entre l'observateur et l'objet observé) est une contradiction dans les termes.

Je pourrais développer ce point en faisant une analyse comparée d'un texte d'Enstein (un article qu'il a écrit sur Bertand Russel) et de la plaidoirie de Kant pour se défendre d'être un idéaliste (au sens que ce terme à en philosophie), si tu souhaites plus de précisions. La plaidoirie de Kant est, dans le fond, une réponse à l'objection que tu m'opposes.

Je suis intéressé par une explication là dessus. ZF est bien fondée dans le sens ou toute compréhension est associée à un ensemble préexistant « Étant donné un ensemble A et une propriété P exprimée dans le langage de la théorie des ensembles, il affirme l'existence de l'ensemble B des éléments de A vérifiant la propriété P. » ce que j’interprète (librement) comme une relation de sous typage. Étant donné que le « x ∈ A » ressemble quand même pas mal à une assertion de type et qu’elle est nécessaire dans une théorie des ensemble, j’ai du mal à comprendre en quel sens ça correspond à un langage dynamique.

Ton interprétation (libre) ne tombe pas loin de la réalité : telle était l'intention primordiale de la théorie, mais c'est « mal » fait. L'idée étant de voir un ensemble comme un concept dont l'extension (la totalité de ses éléments) dénote les objets tombant sous le concept (d'où, par exemple, l'axiome d'extensionnalité affirmant que deux ensembles ayant les mêmes éléments sont égaux), et l'inclusion entre ensembles exprimant alors la subordination entre concepts, c'est-à-dire du sous-typage.

Ma comparaison avec le typage dynamique (comparaison à laquelle j'ajoutais si je peux m'exprimer ainsi) vient du fait que lorsque l'on prend un énoncé universellement quantifié de la théorie, on quantifie sur tout l'univers des ensembles qui se comporte alors à la manière du interface{} du Go. ;-) Raison pour laquelle les auteurs de HoTT écrivent en introduction de leur ouvrage :

In type theory, unlike set theory, objects are classified using a primitive notion of type, similar to the data-types used in programming languages. […]
This rigidly predictable behavior of all objects (as opposed to set theory’s more liberal formation principles, allowing inhomogeneous sets) is one aspect of type theory that has led to its extensive use in verifying the correctness of computer programs.

Ce que j'ai graissé est à mettre en lien avec les reproches adressées à Go d'utiliser le interface{} pour la généricité du code, ce qui ne permet pas de garantir statiquement l'homogénéité d'une liste : il faut écrire des fonctions de constructions qui font du typage dynamique à base de switch sur les types des paramètres.

Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait pour énoncer une propriété des entiers. Ici le quantificateur universel sur x parcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent $x \in \omega$ correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent. Je vois alors l'énoncé comme une fonction qui prend en entrée un interface{} et qui fait du typage dynamique : une assertion de type ou un switch (comme tu veux), comme en Go. En Coq ou en HoTT, on écrirait tout simplement forall (x : Nat) ..., soit pour tout entier, .... La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.

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

Sommaire

• Kant et les théories des types
• Kant et la physique théorique

Kant et les théories des types

Tu peux arguer qu’il est possible de faire la même chose en langage naturel, mais il faut le contraindre de manière à ne garder que les jugements valides dans le système de règle défini. Or il n’a jamais décrit ces contraintes (enfin je te laisse l’infirmer ;).

Ce que tu me demandes (infirmer la chose) est impossible à effectuer dans un commentaire. Tout ce que je peux dire c'est que les liens entre la philosophie kantienne et les théories des types contemporaines sont une évidence pour qui les connaît : elles procèdent toutes de la même approche méthodologique.

Le mieux que je puisse faire dans un commentaire, c'est pointé du doigt quelques références : Per Martin-Löf et Jean-Yves Girard.

Le second est l'auteur, entre autre, du système F qui est un système de types génériques pour le lambda-calcul : c'est le système de type à la base de langages comme Haskell ou OCaml. Sur sa page personnelle (le lien est sur son au-dessus) tu trouveras une partie intitulée La syntaxe transcendantale :

La syntaxe transcendantale est la justification technique des thèses du fantôme de la transparence. Le programme est exposé dans l'article La syntaxe transcendantale, manifeste (Février 2011).

Le livre en question (le fantôme de la transparence) est celui dont j'ai parlé à gasche dans ce commentaire. Je ferais deux remarques là-dessus. Le qualificatif transcendantale est une référence on ne peut plus explicite à Kant, ce dernier ayant utilisé les expressions philosophie transcendantale ou philosophie critique pour qualifier son œuvre philosophique. Ensuite, à la fin de l'introduction du livre, on peut lire :

Le principal bénéficiaire de cette visite non guidée aura été l'auteur, tout surpris d'y trouver matière à de futurs développements techniques. Et de découvrir la surprenante adéquation du kantisme — au sens large — à la logique contemporaine. Ce qui n'est pas très étonnant après tout : que veut dire « raison pure », sinon logique ?

En ce qui concerne Martin-Löf, il est également l'auteur d'une théorie de types dépendants intuitionnistes. Il a participé au groupe de travail ayant écrit la théorie homotopique des types (HoTT) visant à fournir une alternative à ZF pour le fondement des mathématiques basée sur la théorie des types (ça se comprend, ZF c'est l'archétype du typage dynamique; il n'y a qu'un seul type statique : celui d'ensemble, tout le reste est dynamique, si je peux m'exprimer ainsi). Dans l'introduction du livre HoTT, on lit :

Per Martin-Löf, among others, developed a “predicative” modification of Church’s type system, which is now usually called dependent, constructive, intuitionistic, or simply Martin-Löf type theory. This is the basis of the system that we consider here; it was originally intended as a rigorous framework for the formalization of constructive mathematics.

Martin-Löf est aussi l'auteur d'un article : analytic and synthetic judgements in type theory sur la philosophie kantienne des mathématiques. De même l'omniprésence de Kant dans la première des trois conférences qu'il donna sur la logique en 1983 à Siena devrait te mettre sur la piste.

Lorsque l'on s'occupe à notre époque de théorie des types, éluder toute référence kantienne pourrait s'apparenter, pour reprendre une expression utilisée ailleurs dans les commentaires, à une faute professionnelle.

Kant et la physique théorique

Après effectivement on peut arguer que le cerveau fait des calculs de probabilité conditionnelles - http://www.college-de-france.fr/site/stanislas-dehaene/course-2012-02-21-09h30.htm très intéressant au passage - de là a dire que l’invention du concept de causalité est subordonnée à ça, ou si nous étions condamnés à l’inventer …

Je n'ai pas écouté la conférence mais seulement lu le texte qui l'accompagne. Je ferais deux remarques là-dessus :

• l'auteur occupe la chaire de psychologie cognitive expérimentale ;
• le terme « hypothèse » revient à de nombreuses reprises, comme il se doit pour une science expérimentale.

Kant et les kantiens ne pratiquent pas de science expérimentale mais de la science pure ou rationnelle, c'est-à-dire des sciences dont les principes fondamentaux ne sont pas fondés sur l'expérience et l'observation, et dans les sciences expérimentale ne considèrent que la forme nécessaire que doivent prendre leurs théories pour être adéquate à la structure de notre esprit. Tu noteras que je parles d'esprit et non de cerveau : le cerveau est aussi peu le siège de la pensée que le cœur est celui des émotions, si ce n'est par amalgame matérialiste. Dans un tel champ du savoir, le recours aux hypothèses est mal venu :

Pour ce qui concerne la certitude, voici la loi que je me suis imposée à moi-même : dans cette sorte de considération, l'opinion n'est en aucune façon permise, et tout ce qui ressemble seulement à une hypothèse est une marchandise prohibée, qui ne doit pas être mise en vente à bas prix, mais doit être saisie aussitôt que découverte. Car toute connaissance qui doit être établie a priori donne d'elle même à entendre qu'elle veut être tenue pour nécessaire; plus encore en ira-t-il d'une détermination de toutes les connaissances pures a priori, qui doit être la mesure et par la même l'exemple de toute certitude apodictique (philosophique).

Kant, Critique de la Raison Pure.

Avoir recours à des hypothèse dans ce genre d'enquête, ce serait comme vouloir fonder la mathématique sur des conjectures : ce n'est pas sérieux.

Maintenant, comme exemples de personnes ici du monde de la physique ayant écouté l'appel de Kant, je citerai :

• freejef et son laboratoire de Lille, d'après l'introdution de sa dépêche sur le recalage et la corrélation d'images ;
• Thibault Damour membre de l'académie des Sciences et spécialiste de relativité générale, d'après son texte sur la question Le temps passe-t-il ? (voir page 9)
• des épistémologues et physiciens d'après la conclusion du livre Petit voyage dans le monde des quanta d'Étienne Klein :

Certes les problèmes de fond posés par Bohr, Heinsenberg, Einstein, Schrödinger ou Pauli restent d'actualité, mais on dispose aujourd'hui pour les traiter de davantage de résultats et de davantage d'arguments. Plusieurs systèmes épistémologiques essaient d'intégrer ces nouvelles donnes : la thèse du réel voilé de Bernard d'Espagnat, le solipsisme convivial d'Hervé Zwirn, le réalisme physique de Michel Paty, et de façon plus diffuse le réalisme ouvert, l'opérationnalisme, le phénoménalisme, et enfin l'idéalisme, lui-même divisé en idéalisme radical et idéalisme modéré, les deux pouvant être plus ou moins kantiens…

E. Klein, Petit voyage dans le monde des quanta.

J'ajouterai simplement qu'une telle situation n'a rien d'étonnant quand on connaît certaines résultats de la physique quantique et le contenu de la philosophie kantienne. Je conclurai sur la réponse d'un kantien à un extrait du livre d'Étienne Klein :

En premier lieu, s'il est vrai que le vecteur d'état contient tout ce que l'on peu savoir d'un système quantique, autrement dit si le formalisme est complet, il faut admettre qu'un phénomène ne peut être interprété comme fournissant des informations concernant des propriétés qu'auraient les objets eux-mêmes, indépendamment de la connaissance que nous en avons. Songeons à une pierre. C'est un objet qui existe « pleinement » au sens où nous n'hésitons pas à lui attribuer par la pensée des propriétés bien définies : une taille, une forme, une couleur qui sont ce qu'elles sont, même en l'absence d'observateur. Les objets quantiques, eux, ne semblent pas pouvoir être considérés de la sorte puisque leurs propriétés ne sont pas toujours déterminées antérieurement à la mesure qui en est faite.

Ce qui choque un Kantien n'est pas ce qu'il dit des objets quantiques, mais ce qu'il dit de la pierre ! :-P

Les objets que nous observons, en tant qu'objets de la connaissance expérimentale, n'ont aucune existence propre indépendante de nous. Si nous voyons partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous-même (voir l'article de Thibault Damour). Ainsi, lorsque l'on fait abstraction de tout rapport à l'expérience possible alors l'espace et le temps s'évanouissent, ce qui nous apparaît comme une pierre dans l'expérience devient un quelque chose d'inconnu, qui nous restera à jamais inconnaissable, une chose ineffable (dont on ne peut parler). L'avantage du kantisme sur toute autre approche épistémologique est qu'il ne fait aucune distinction ontologique entre la pierre et les objets quantiques : ce ne sont que de simples phénomènes qui n'ont pas d'existence propre en dehors de leur rapport à un observateur.

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

Il y a quand même une légère différence dans les détails :)

Pas spécialement, le principe que je décris est celui qu'a utilisé Gödel pour démontrer son fameux théorème d'incomplétude : une théorie assez riche (au pouvoir expressif suffisant) pour parler d'elle même a toujours des énoncés indécidables (qu'elle ne peut ni prouver ni réfuter) et parmi ceux-ci figurent toujours sa propre cohérence (sa non contradiction). Ce que je dis c'est que si une théorie est assez riche (comme l'est ZF) pour exprimer les principes de la théorie des modèles et donc parler de la relation entre la forme et le contenu (ce en quoi consiste la vérité) alors elle ne peut engendrer son propre contenu (elle ne peut construire un modèle d'elle même) et fournir un critère matériel et universelle de la vérité, sous peine d'être incohérente d'après le théorème d'incomplétude. Dans ce cas, comme elle peut prouver tout et n'importe, on ne peut nullement avoir confiance dans ce qu'elle prétend affirmer.

Cette démarche consiste à réfléchir la métathéorie dans la théorie elle même, c'est le même genre d'argument qu'a utilisé Turing pour prouver l'impossibilité de résoudre le problème de l'arrêt pour sa machine universelle. D'un point de vue programmation, cela revient à dire qu'un langage ne peut se compiler lui-même sans une phase de bootstrap : il faut un coup de pouce extérieur au langage de programmation.

J’ai l’impression que tu décris une sorte de « principe de réflexion » de la pensée abstraite dans la logique formelle, comme dans l’univers constructible de Gôdel ( http://www.madore.org/~david/weblog/d.2013-03-19.2124.constructible.html ) ou les ensembles et leur structure décrit par un rang inférieur se reflètent dans les rangs supérieurs de différentes manières.

L'univers des constructibles de Gödel sert à prouver des théorèmes de consistance relative : si ZF est non contradictoire alors il en est de même de ZF augmentée de l'axiome du choix, ce dernier axiome n'introduit pas de contradiction dans la théorie. C'est du même ordre que les théorèmes de consistance relative que Poincaré a effectués au XIXème entre les géométries euclidienne et non euclidiennes. Le cercle de Poincaré, construit dans un espace euclidien, permet d'interpréter les axiomes de la géométrie hyperbolique. Autrement dit, si la géométrie euclidienne est cohérente alors il en est de même de l'hyperbolique.

En revanche aux questions : l'arithmétique est-elle cohérente ? la géométrie est-elle cohérente ? ZF est-elle cohérente ? la logique et son principe de contradiction est incapable d'y répondre. La seule chose qu'elle peut faire c'est prouver la cohérence d'une théorie en admettant la cohérence d'une autre. Par exemple, on peut prouver la cohérence de l'arithmétique à partir de ZF, mais reste la question : ZF est elle cohérente ? On peut continuer en ajoutant des axiomes de grands cardinaux qui prouvent la consistance de ZF (ils fournissent un modèle de celle-ci), mais reviens alors la question : ses nouveaux axiomes sont-ils cohérents ? Et cette approche turtles all the way down la logique formelle ne peut en sortir, pour la simple raison que, laissée à elle même, elle n'engendre que des tautologies (l'art de M. de La Palice) et est incapable de répondre à la question : comment des jugements synthétiques a priori sont-ils possibles ?

Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)

Ça se discute, ils ne sont nullement enrichis, ce sont les mêmes mais exprimés dans une langue différente. Un principe ne deviendrait ni plus vrai, ni plus clair, ni plus riche sous prétexte qu'il serait exprimés en français plutôt qu'en anglais (ou vice versa). La méthode kantienne est on ne peut plus formelle (il n'y a pas plus formaliste qu'un kantien), et les langues naturelles sont tout à fait adaptées pour exprimer de tels principes. Il n'est pas nécessaire de recourir à des symbolismes compréhensibles par une machine (ce qui n'est d'ailleurs adapté qu'à la formalisation de la pensée mathématique mais nullement à la pensée philosophique, comme les problèmes de philosophie du droit) pour formaliser sa pensée : je préfère de loin l'usage du français à Coq, par exemple. Les langues naturelles ont, en leur sein, un système à type dépendant mais une grammaire plus complexe que les grammaires régulières des langages de programmation (il suffit de voir la difficulté que rencontre l'auteur de grammalecte, ou tous ceux qui travaillent sur le traitement automatique des langues).

Prenons, un principe de base de la logique de Hoare utilisée pour la formalisation des langages impératifs, celui de la composition des instructions :

{ P } S { Q }  { Q } T { R }
----------------------------
    { P }  S ; T { R }

une expression de la forme { P } S { Q } se lit : l'instruction S fait passer le système de l'état P à l'état Q. Une telle règle ce lit alors : si l'instruction S fait passer la machine de l'état P à l'état Q et que l'instruction T fait passer de l'état Q à l'état R, alors la série d'instructions S ; T fait passer de l'état P à l'état R.

Il se trouve que c'est l'analogue dans le paradigme de la programmation fonctionnelle pure de la composition des fonctions :

fun f g x -> g (f x);;
- : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = <fun>

A --> B    B --> C
------------------
     A --> C

Autrement dit, des deux prémisses si A alors B et si B alors C, on conclue à si A alors C. Cela résulte d'une double application de la règle dite du modus ponens :

• si A alors B, or A donc B (modus ponens utilisant la première prémisse et l'hypothèse A)
• si B alors C, or B donc C (modus ponens utilisant la seconde prémisse et la conclusion du syllogisme hypothétique précédent)

ainsi en supposant A on conclue à C, c'est à dire que l'on a prouvé si A alors C. Ce genre de preuve, quelque peu pédante, est ce que nous oblige à écrire Coq (il offre quand même des techniques pour éviter de rentrer autant dans les détails).

Ce que Kant a prouvé, par exemple, dans la Critique de la Raison Pure c'est que le concept de cause (qui sert à expliquer les changements d'états des choses réelles dans le monde physique) n'est pas un concept d'origine empirique, mais un concept que nous imposons nous même à la nature en vertu de la structure formelle de notre esprit et qu'il a pour type (là j'emploie une terminologie contemporaine) la forme logique des jugements hypothétiques (si A alors B).

On pourrait exprimer le principe fondamentale de la dynamique de Newton ainsi dans un tel symbolisme : { p } F { p + F * dt}. Autrement dit, un corps dans l'état de mouvement p et soumis à une force F se retrouve dans l'état { p + F * dt } au bout d'un temps infiniment petit dt. L'on retrouverait ainsi les considérations entre les sémantiques petit pas (small step) ou grands pas (big step), auxquelles gasche faisait allusion dans ce commentaire, et la distinction entre les lois différentielles et les lois intégrales en physique théorique. La première étant une approche discrète (sémantique des langages de programmation), là où la seconde est continue (physique théorique).

Et c'est ce lien formel entre le principe de causalité et la forme des jugements hypothétiques qui explique que l'on peut construire des machines qui « exécutent » les calculs automatiquement.

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

La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. […] Mais du point de vue de la cohérence, ça peut lever des lièvres.

Oui car telle est son affaire, elle peut montrer l'incohérence d'une formalisation. Pour ce qui est de prouver la cohérence, par contre…

Ça me rappelle ce passage humoristique dans la partie remerciements de la thèse de Perthmâd (qui, s'y j'en crois les notes de publication de la toute récente dernière version de Coq, a fait un gros travail de nettoyage et d'optimisation du langage des tactiques) :

— Un thésard demanda à Hugo Herbelin : « Coq est-il cohérent ? »
— Anomaly: Uncaught exception Mu.

Par malheur, l’histoire omet de raconter si l’étudiant fut illuminé ou bien s’il l’était déjà à l’instant même où il songea à passer un doctorat d’informatique fondamentale 5 [1].

[1]Par contre, l’histoire précise bien que le rapport de bug qui s’en suivit fut marqué WontFix par un certain kgoedel. Ce n’est pas dans le privé qu’on verrait ça.

Dans une démarche également historique, le passage que j'ai cité de la Critique de la Raison Pure est extrait du paragraphe sur la question « Qu'est-ce que la vérité ? » qui commence ainsi :

La vielle est célèbre question, par laquelle on se figurait pousser les logiciens dans leur retranchement et on cherchait à les amener, ou à devoir se laisser surprendre dans un pitoyable diallèle, ou bien à devoir avouer leur ignorance, et par la suite la vanité de tout leur art, est celle-ci : Qu'est-ce que la vérité ? La définition nominale de la vérité, qui en fait la conformité de la connaissance avec son objet, est ici accordée et supposée; mais on veut savoir quel est le critère universel et sûr de la vérité de toute connaissance.

C'est déjà une grande et nécessaire preuve de sagesse et de pénétration que de savoir ce que l'on doit raisonnablement demander. En effet, si la question est absurde en soi et si elle appelle parfois, outre la confusion de celui qui la soulève, l'inconvénient de porter à des réponses absurdes l'auditeur qui n'est pas sur ses gardes, et de donner ainsi le ridicule spectacle de deux personnes, dont l'un trait le bouc (comme disaient les anciens), tandis que l'autre tend un tamis.

Si la vérité consiste dans l'accord d'une connaissance avec son objet, cet objet doit être par là distinguer des autres; car une connaissance est fausse, si elle ne s'accorde pas avec lequel elle est rapportée, alors même qu'elle pourrait bien valoir pour d'autres objets. Or, un critère universel de la vérité serait celui qui vaudrait pour toutes les connaissances, sans distinction de leurs objets. Mais il est clair, puisqu'on y fait abstraction de tout contenu de la connaissance (du rapport à son objet), et que la vérité à trait justement à ce contenu, qu'il est tout à fait impossible et absurde de demander une marque de la vérité de ce contenu des connaissances, et qu'on ne peut donc proposer une caractéristique suffisante et en même temps universelle de la vérité. Comme nous avons déjà nommé plus haut le contenu de la connaissance sa matière, on devra dire : On ne peut demander aucune caractéristique universelle de la vérité quant à sa matière, parce que c'est en soi contradictoire.

Kant, Critique de la Raison Pure.

On trouve des considérations identiques dans le traité qu'il consacra à la logique. Premièrement, ce qu'il appelle la définition nominale de la vérité est celle que l'on utilise toujours de nos jours sous le nom de définition tarskienne de la vérité à la base de la sémantique tarskienne (utilisée en théorie des modèles). Ensuite, si l'on combine le théorème de Gödel auquel Perthmâd fait allusion (le théorème d'incomplétude) à une autre théorème fondamentale de Gödel (son théorème de complétude : une théorie est cohérente si et seulement si elle a un modèle), on aboutit à la conclusion du texte kantien cité ci-dessus. Une théorie (disons ZF, la théorie axiomatique des ensembles) qui fournirait un critère matérielle de sa vérité serait en mesure d'engendrer son propre contenu (fournirait un modèle d'elle-même), serait donc cohérente (en vertu du théorème de complétude) ce qui contredirait le théorème d'incomplétude.

Le théorème d'incomplétude clos une période historique au cours de laquelle la thèse centrale de la Critique de la Raison Pure fut attaqué de toute part par des logiciens, et Gödel finit par donner raison à Kant. :-)

On gagne déjà beaucoup à pouvoir faire tenir une foule de recherche sous la formule d'un seul problème. Par là, en effet, on ne facilite pas seulement pour soi-même son propre travail, en se le déterminant avec précision, mais on rend aussi plus facile à quiconque veut l'examiner de juger si nous avons ou non satisfait à notre dessein. Le problème propre de la raison pur est donc contenu dans la question suivante : Comment des jugements synthétiques a priori sont-ils possibles ? […]

Dans la solution du problème précèdent est engagée en même temps la possibilité du pur usage de la raison pour fonder est développer toutes les sciences qui contiennent une connaissance théorique a priori des objets, c'est-à-dire la réponse à ces questions :

• Comment la mathématique pure est-elle possible ?
• Comment la physique pure est-elle possible ?

Kant, ibid.

À cette subdivision de la question, précède le texte suivant :

Les jugements mathématiques sont tous synthétiques. Cette proposition semble avoir échappé jusqu'ici aux observations des analystes de la raison humaine, et même être exactement opposée à toutes leurs conjectures, bien qu'elle soit incontestablement certaine et très importantes dans ses conséquences. En effet, comme on trouvait que tous les raisonnements mathématiques procédaient tous d'après le principe de contradiction (ce qu'exige la nature de toute certitude apodictique) on se persuada que les principes étaient connu aussi étaient connus à partir du principe de contradiction : en quoi ces analystes; car une proposition synthétique peut bien être saisie d'après le principe de contradiction, mais seulement de telle sorte qu'une autre proposition synthétique soit supposée, d'où elle puisse être déduite, mais jamais en elle-même.

Kant, ibid.

Ce qu'a prouvé Gödel, c'est que la logique formelle (et donc le principe de contradiction) ne peut légitimer à elle seule le raisonnement par récurrence : le principe du raisonnement par récurrence est un pur jugement synthétique a priori.

Il y a un membre de linuxfr qui a pour signature quelque chose du style : «BeOS le faisait déjà il y a vingt ans ». Pour ma part, d'une manière générale, je dirais : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. Par exemple, la logique de Hoare utilisée par frama-c, c'est dans la Critique de la Raison Pure; ou bien la programmation par contrat, la gestion de propriété des espaces mémoires par Rust ou Mezzo, c'est dans la Doctrine du Droit (que l'on peut voir comme une théorie de typage du droit romain). :-)

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

Tout le monde doit avoir une adresse email non-pipeau chez pasBig pasBrother

Tu sous-entend que pasBillpasGates devrait administrer un serveur mail et offrir une adresse à chaque membre de linuxfr ? :-D

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

Petit ajout que j'ai oublier de préciser avec le type contradictoire.

type contradiction = { faux : 'a. 'a; }

let i = {faux = Obj.magic 1};;
val i : contradiction = {faux = <poly>}

(* là c'est bon *)
1 + i.faux;;
- : int = 2

(* là ça segfault !! *)
1.5 +. i.faux;;

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

Juste concernant Go, il me semble que l'approche (en tout cas des critiques que j'ai pu lire ici et là) n'est pas type-safe dans le sens où interface{} serait en réalité le type top comme la classe Object en Java - ce qui permet de facilement bypasser le système de type de Go.

C'est type-safe le interface{}, c'est un type existentiel. Par contre tu perds la garantie du typage statique et tu dois faire des assertions de type ou du switch sur type : il faut faire du typage dynamique. C'est comme en Python, en somme, sauf qu'en dehors de interface{} on a bien la garantie d'un typage statique (sans quantification universelle sur les types, c'est-à-dire, sans généricité mais c'est déjà pas trop mal). En gros, je le vois comme ça (je me trompe peut être) :

type intf = E : 'a -> intf
let i = E 1

mais comme Go garde des informations de typages au runtime, on peut retrouver à l'éxecution la valeur contenue dedans avec son type : pour Go, i est de type int et vaut 1.

var i interface{}
i = 1
fmt.Printf("i est de type %T et vaut %v", i, i)
// affiche : i est de type int et vaut 1

Ce qui n'est pas type-safe, c'est une valeur de tout type (avec quantification universelle sur les types). On parle de l'aspect unsound du système de type de Java (qui a des génériques) ou de la valeur undefined de Haskell ?

type contradiction = {faux : 'a. 'a}

let i = {faux = Obj.magic 1};;
val i : contradiction = {faux = <poly>}

Là, on contourne clairement le système de types, mais on annonce la couleur en utilisant le module Obj. ;-) Le type de faux, c'est le principe ex falso quodlibet.

Par contre j'ai un peu trop surestimé le système des interfaces : j'ai cru que c'était du type classes à la Haskell mais sans types paramétriques. En fait non, c'est clairement moins bien fait, tu ne peux pas avoir d'interface pour de telles méthodes :

type Vertex struct {
    X, Y float64
}

func (v *Vertex) Add(w *Vertex) Vertex {
  return Vertex{v.X + w.X, v.Y + w.Y}
}

func Add(v Vertex, w Vertex) Vertex {
    return v.Add(&w)
}

func main() {
    v := Vertex{3, 4}
    w := Vertex{5, 9}
    fmt.Println(Add(v,w))
} // affiche {8 13}

On ne peut pas définir le type interface de ceux qui implémentent la méthode Add : c'est nul et ça pourrait limiter le besoin de recourir à interface{}. Déjà qu'il n'ont pas de génériques (types paramétriques), ils auraient pu faire un effort de ce côté là.

En OCaml :

type 't add = { add : 't -> 't -> 't; }
type vertex = {x : float; y : float}

let add_vert = {add = fun v w -> {x = v.x +. w.x; y = v.y +. w.y}};;
val add_vert : vertex add = {add = <fun>}

let add_int = {add = (+)};;
val add_int : int add = {add = <fun>}

let add {add} x y = add x y;;
val add : 'a add -> 'a -> 'a -> 'a = <fun>

add (add_vert) {x =3. ; y = 4.} {x = 5. ; y = 9.};;
- : vertex = {x = 8.; y = 13.}

add (add_int) 3 4;;
- : int = 7

Le mécanisme des arguments implicites (s'il était implémenté) permettrait d'inférer automatiquement le 'a add à utiliser en fonction du type 'a des autres paramètres passés à add par unification, là où pour l'instant on doit le passer explicitement (c'est ce que font les types classes de Haskell mais en plus général, les types pouvant être paramétriques comme avec les monades). Go fait cela mais de manière très restreinte : la variable de type 't ne doit pas apparaître dans le type des champs de l'enregistrement. /o\

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

Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.

C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.

Je sais bien que tu n'ignores pas les exigences en question, mon conseil de visionnage était là pour te dire que Xavier Leroy non plus, que son projet s'inscrit dans cette démarche d'exigence (raison pour laquelle il aborde le secteur de l'aéronautique), et que tu pourras peut être comprendre en quoi ce logiciel est une avancée dans la recherche de sécurité par rapport aux méthodes antérieures — celles que tu connais déjà, justement.

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

Je crois bien que le ton de nos échanges est monté par ma faute, j'en suis désolé. J'étais mal luné l'autre jour, j'aurais du tourner mes doigts dix fois avant d'écrire, j'en suis désolé. :-/

Le bug peut être également dans le model.

Tout à fait, mais cette problématique est hors de portée de la logique et des approches formelles.

Cette partie de la logique de notre connaissance peut donc être nommée analytique, et elle est la pierre de touche, du moins négative, de la vérité, puisqu'il faut d'abord contrôler et estimer d'après ces règles toute connaissance selon sa forme, avant de l'examiner selon le contenu pour établir si, à l'égard de l'objet, elle contient une vérité positive. Mais, comme la simple forme connaissance, aussi d'accord qu'elle puisse être avec les lois logiques, ne suffit (nullement) pour établir la vérité matérielle (objective) de la connaissance, personne ne peut se hasarder de juger des objets avec la simple logique, et à en affirmer quelque chose, sans en avoir entrepris auparavant une étude approfondie en dehors de la logique, pour ensuite essayer simplement de les utiliser et de les lier en un tout cohérent selon les lois logiques, mieux encore, des les examiner simplement d'après elle. Cependant, il y a quelques choses de séduisant dans la possession d'un art aussi spécieux, celui de donner à toute nos connaissances la forme de l'entendement, quelque vide et pauvre qu'on puisse être à l'égard de leur contenu, que l'on use de cette logique générale, qui est simplement un canon pour l'évaluation, comme d'un organon pour produire réellement, du moins en en donnant l'illusion, des affirmations objectives, ce qui est en fait abuser de cette logique.

Kant, Critique de la Raison Pure.

La partie graissée correspond à ce que tu dis : si l'erreur est dans le modèle (le contenu, la matière), la logique qui ne s'occupe que de la forme ne peut rien y faire. Pour grossir le trait, la logique n'a rien à reprocher au raisonnement suivant :

• les hommes sont immortels
• or je suis un homme
• donc je suis un immortel

celui qui se croirait immortel, en se justifiant du fait que la logique ne trouve rien à redire à ce syllogisme, ferait rire n'importe qui face à lui. :-D

Pour faire une analogie avec le domaine juridique : la logique s'occupe des vices de forme dans la procédure. En l'absence de vice de forme, il faut tout de même un procès pour débattre de l'issue du cas : on y examine la question de droit (la majeure du raisonnement : les hommes sont immortels) et la question de fait (la mineure du raisonnement : je suis un homme). Ici, la majeure est en tort : l'accusé est innocenté, déclaré non coupable, ou plutôt non immortel. La question de fait en revanche ne fait ici pas de doute; en cas de non lieu c'est celle-ci qui n'a pu être justifiée.

J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.

Tout à fait : c'est bien pour cela que je parlais d'un travail de titan ! Il faut formaliser les instructions assembleurs (de trois architectures qui plus est : PowerPc, ARM et x86), formaliser la sémantique d'un sous-ensemble assez large du C, puis prouver que toutes les transformations-traductions du code préservent les sémantiques. Mais Xavier Leroy et son équipe on pu réaliser cet exploit (car s'en est un, une première au monde pour un compilateur) parce qu'ils avaient déjà un forte expérience dans l'écriture de compilateur et de sémantique des langages de programmation : ils en avaient entrepris auparavant une étude approfondie en dehors de la logique. ;-)

J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.

Nulle condescendance dans mon message, je mets cette réaction sur le dos du ton que prenaient nos échanges. Je ne suis pas sans savoir comment cette question est gérée en l'absence d'un tel outil, mais je tiens à signaler que la garantie que CompCert apporte sera à jamais inaccessible à ces méthodes. Raison pour laquelle Gérard Berry, qui n'ignore pas non plus ces méthodes, a écrit :

Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.

Le graissage est de moi pour bien souligner que les méthodes auxquelles tu fais allusion, si elle sont acceptées en pratique, ne pourront jamais apporter ce niveau de garanti (j'espère que tu m'épargneras un débat épistémologique sur la distinction entre la connaissance rationnelle et la connaissance expérimentale afin de justifier cette position).

Je tiens à préciser à nouveau que ce compilateur fait partie de la chaîne d'outils que AbsInt vend à ses clients dont Airbus. :

1. Check your C code for runtime errors with Astrée.
2. Compile the code using CompCert
3. Check your stack usage with StackAnalyzer
4. Analyze the execution time with aiT

Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier.

Bien sûr que j'ai le compris : un tel outil doit savoir cacher ses entrailles pour exposer à l'utilisateur ses concepts métiers pour qu'il se focalise sur ce qu'il connaît. Il n'empêche que sous le capot, c'est de la traduction mathématique et de la preuve mathématique, quand bien même l'utilisateur n'en a pas conscience. Un bon outil est celui qui sait se faire discret sur son fonctionnement : celui qui l'utilise, celui qui le construit et celui qui le répare sont rarement les mêmes personnes, n'ont pas les même savoir, ni les mêmes compétences.

D'ailleurs pour illustrer la chose : je ne connaissais pas Go, si ce n'est de nom. Résultat je suis allé jeter un coup d'œil, et bien je trouve leurs choix tout sauf bêtes contrairement à ce que certains ont pu dire. Il n'y a certes pas de généricité (sauf sur quelques types comme les tuples ou les tableaux) mais leur système de type interface est très ingénieux et semble compenser allègrement à l'usage l'absence de généricité. D'un point de vue formel, au premier abord (je n'ai pas creusé plus que cela) ça s'apparente grandement à des fonctions avec arguments implicites sur du lambda-calcul simplement typé avec enregistrements (un langage avec des fonctions comme citoyen de première classe pour lequel un argument de certaines fonctions est inférer par le compilateur)¹. Le polymorphisme au lieu d'être paramétrique (comme C++, Java, Haskell…) et ad-hoc mais vérifier à la compilation. Choix qui offre aux développeurs un large panel de technique de programmation sans l'assomer avec des abstractions difficiles à comprendre, donc à maîtriser et donc à utiliser (comme le sont les modules ou les GADT pour toi).

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

Les classes de type marchent assez bien pour gérer le type Dyntype a, parce que c'est typiquement le genre de valeurs que tu veux passer implicitement, et pour lequel tu n'as pas envie/besoin d'avoir plusieurs implémentations pour un même type.

On en revient toujours au fait que les modules implicites seraient une fonctionnalité géniales pour OCaml. Elle rendrait les modules encore moins citoyen de seconde classe que ne le font les first-class modules. ;-)

Lorsque j'avais mentionné à Leo White l'article-tutoriel sur les structures canoniques en Coq, il m'a répondu l'avoir déjà lu (effectivement, cela fait même partie des références de l'article de présentation du prototype sur les modules implicites). Cela étant, ils mentionnent un autre article intéressant, qui pourrait servir de base pour la formalisation, dans leurs références : The Implicit Calculus: A New Foundation for Generic Programming qui mentionne aussi le tutoriel sur les structures canoniques. Mais il me vient à l'esprit une interrogation :

• l'article sur le calcul implicite se limite au système F ;
• les auteurs précisent que les structures canoniques n'ont pas été formellement spécifiées ;
• le mécanisme des arguments implicites est décrit pour tous les système du lamda-cube dans la partie 4 de la thèse de Amokrane Saïbi (en français \o/).

S'il est vrai que dans sa thèse il décrit un algorithme d'unification plutôt qu'une formalisation à base de règles d'inférence à la Gentzen, les deux approches ne me semblent pas si éloignées et je ne vois pas ce qu'il manque à ce système pour fournir ce dont ont besoin les modules implicites pour synthétiser les arguments implicites.

Dans un autre registre, sur le statut des modules dans le langage : que penses-tu des travaux de Rossberg, Russo et Dreyer sur 1ML présentés à l'ICFP en 2015 ? Cela demanderait trop de modifications à apporter au langage pour avoir cela dans OCaml ?

An alternative view is that 1ML is a user-friendly surface syntax for System Fω that allows combining term and type abstraction in a more compositional manner than the bare calculus.

et ça résoudrait les incompréhensions de Nicolas Boulay, ils y définissent les modules avec la syntaxe des enregistrements. ;-)

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

compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?

Bien sur que non, c'est un travail de titan le code complet ! C'était pour illustrer ma proposition « la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types », en montrant un système de types tel que son expressivité dispense d'avoir à recourir à des tests unitaires. Ce théorème, qui n'est qu'une infime partie du code du compilateur, est celui que Xavier Leroy utilise dans sa vidéo comme illustration : c'est normal, c'est lui qui exprime que son compilateur est optimisant est n'apporte aucune modification de comportement à la compilation (si il y a un problème dans le code compilé, il se trouve déjà dans le code C).

Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne".

Je le sais bien, c'est pour cela que j'ai parlé de cette industrie. Au sujet du projet CompCert C, Gérard Berry (lui, tu le connais il a cofondé l'entrepise qui fut (est ?) ton employeur et est le père du langage Esterel) l'a décrit dans le bulletin de la société informatique de France ainsi :

CompCert, l’autre grande contribution de Xavier Leroy et de son équipe, est une aventure encore unique sur le plan mondial. Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.

Pour info le compilateur est un produit (il n'est pas libre, seulement pour un usage non-commercial) de l'entreprise AbstInt :

Certification and qualification

Current safety standards such as ISO 26262, DO-178B/C, IEC-61508, EN-50125 and others require identifying potential functional and non-functional hazards and demonstrating that the software does not violate the relevant safety goals.

Abstract-interpretation based tools such as aiT, StackAnalyzer, and Astrée provide formal veri­fi­cation with 100% complete and reliable results. They are therefore perfectly suited to be used for certification.

The qualification process is greatly simplified by our Qualification Support Kits. Additionally, Qualification Software Life Cycle Data Reports provide de­tails about our development processes.

qui a pour client Airbus et pour partenaire Esterel Technologies. ;-) Pour Airbus, ils utilisent leurs analyseurs statiques de code (aiT analyse le comportement temporel, StackAnalyzer l'absence de stack overflow et Astrée l'absence de runtime error) :

For many years Airbus France has been using aiT, StackAnalyzer and Astrée in the devel­op­ment of safety-critical avionics software for sever­al airplane types, including the A380, the world’s largest passenger aircraft. The analyzers are used as part of certifi­cation strategy to demonstrate compliance to DO-178B, up to Level A.

et Compert C s'incrit dans la chaîne des outils : si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?

Je crois que je peux te répondre la même chose, mais pas pour le même domaine.

T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?

Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).

T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)

Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.

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

ton exemple n'a rien à voir avec un truc réel.

Tu te fous de moi !!! C'est du Coq et c'est extrait du code du compilateur CompCert C. Cet extrait est le théorème fondamental qui garantie la certification du compilateur. C'est pour des industriels qu'il a été développé (aéronautique entre autre).

Pour le reste des échanges, j'arrête là : je pisse dans un violon, tu ne connais pas grand chose aux sujets abordés mais tu parles quand même, ça me saoule.

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

Le problème est que tu n'attrapes pas grand chose comme erreur avec un système de typage.

Et les licornes roses ont de jolies ailes ! :-D

Tu te rends compte de ce que tu viens d'écrire ? D'une la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types, et de deux on peut pousser le système jusqu'à permettre de se dispenser totalement de tests unitaires. Exemple :

Theorem transform_c_programm_preservation :
  forall p tp beh
  transf_c_program p = Ok tp ->
  program_behaves (Asm.semantics tp) beh ->
  exists beh', programm_behaves (C.semantics p) beh'
            /\ behavior_improves beh' beh

Traduction en français : pour tout programme C p, tout programme assembleur tp et tout comportement observable beh, si la fonction transf_c_prgram appliquée à p renvoie le programme tp et que beh est un comportement observable de tp en accord avec la sémantique ASM, alors il existe un comportement observable beh' de p conforme à la sémantique du C et tel que beh améliore beh'.

Autrement dit : la fonction transform_c_program est un compilateur optimisé du C vers l'assembleur préservant la sémantique du code source et certifié conforme ! Pas besoin de faire de tests unitaires : quand dans l'énoncé on quantifie sur tous les programmes et tous les comportements, on parle bien de l'infinité des programmes et des comportements possibles (on ne peut pas faire des tests unitaires sur une infinité de cas). :-)

Tu noteras au passage la notation transform_c_programm_preservation : blabla où blabla est tout à la fois le type et l'énoncé du théorème. ;-)

Plus de détails et de compléments dans la vidéo In search of software perfection - 2016 Milner Award lecture by Dr Xavier Leroy..

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

Donc au delà de l'apprentissage, il faut peut être des outils pour aider à appréhender la logique et éviter aussi de faire tomber le cerveau dans des pièges. Par exemple pour moi le développement avec des tests unitaires m'aide souvent : il me montre via des exemples que je suis encore tombé dans le panneau de mon intuition !

Le typage statique est un tel outil. La plupart des systèmes de types n'évitent pas la nécessité de recourir à des tests unitaires, mais ils permettent de capturer certaines erreurs de raisonnement. Que la logique expose les lois de notre pensée ne signifie (malheureusement) pas que nous les respectons toujours, les erreurs de raisonnement sont plus ou moins fréquentes selon les personnes.

J'avoue j'ai un peu placé la référence au jeu car il m'a bien plu :-)

Il m'a bien plu aussi, merci pour le partage. Si l'on reprend, par exemple, le niveau 4, celui-ci illustre les problèmes de concurrence d'accès aux ressources. On a un processus (steve) qui s'accapare toutes les resources (de type female), pose un verrou dessus et ne les libère jamais. La solution : créer une ressource qui le tue avant qu'il ne bloque l'accès aux autres. :-)

Ceci dit en tant que programmeur je suis souvent le gardien de la logique des spécifications fonctionnelles, et je peux dire que c'est un métier difficile ! Réussir à expliquer au client que ce qu'il demande pose des problèmes de logique… c'est constant dans le métier de l'informatique.

Je veux bien te croire qu'il s'agit là d'une tâche difficile.

La plupart de ces incohérences n'apparaissent d'ailleurs que quand on est en train d'écrire le programme… (ça ne ment pas) !

Comme lorsque l'on cherche à véritablement démontrer une proposition qui, au premier abord, nous semblait évidente ou plus que plausible. ;-)

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

Les usages poussés du système sont effectivement compliqués, mais cela me semble en grande partie inhérent aux concepts même de modules. Cela ne m'étonne pas qu'il soit très difficile de faire un bon système de modules.

Cela étant, si les utilisateurs de Go aimeraient avoir un équivalent dans le langage (comme semble l'exprimer Nicolas Boulay), ils peuvent toujours renvoyer les concepteurs du langage à l'article de Xavier Leroy A modular module system ;-)

Abstract

A simple implementation of an SML-like module system is presented as a module parameterized by a base language and its type-checker. This implementation is useful both as a detailed tutorial on the Harper-Lillibridge-Leroy module system and its implementation, and as a constructive demonstration of the applicability of that module system to a wide range of programming languages.

C'est moi qui graisse.

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

Mais je trouve que leur forme dans ocaml est très complexe et très peu lisible.

J'ai fini par m'y habituer, mais il est vrai que le langage des modules et foncteurs est assez verbeux. Après sur la syntaxe concrète de définition d'un module sans paramètre, je ne vois pas bien la différence entre l'usage d'accolades ou celle de mots-clés :

module type M = sig
  type t
  val v : t
end

(* VS *)

module type M = {
  type t ;
  v : t ;
}

Par exemple, en Coq, où la distinction entre type et valeur n'a pas lieu d'être (les types sont des valeurs comme les autres et vivent dans le même monde), on utilisera la syntaxe des enregistrements pour écrire cela (même si Coq a aussi son système de modules).

Record M : Type  := mkM {
  t : Type ;
  v : t ;
}.

Quoi qu'il en soit, je ne trouve pas la syntaxe concrète pour écrire des modules ou leur signature si illisible que cela. Même dans les usages simples des foncteurs (qui sont des fonctions des modules vers les modules), je trouve la notation assez proche du langage des fonctions du langage.

(*
  une signature pour exprimer la possibilité de
  convertir un type quelconque vers un string :
  c'est la donné conjointe d'un type et d'une
  fonction de conversion.
*)

module type Showable = sig
  type t
  val show : t -> string
end

(*
  à partir d'un tel module, il n'est pas difficile
  de définir des fonctions pour afficher le type
  à l'écran. On passera par un foncteur.

  On commence par étendre la signature précédente
  pour ajouter des fonctions d'affichage, puis celle
  du foncteur qui transforme un module du premier genre
  dans le second
*)

module type Printable = sig
  include Showable
  val print : t -> unit
  val println : t -> unit
end

module type Print_abs = functor (M : Showable) -> Printable
module type Print = functor (M : Showable) -> Printable with type t = M.t

Ici, c'est là que le langage commence à devenir verbeux, mais c'est par nécessité. Un module permet de cacher au monde extérieur la représentation concrète de ses types : pour faire en sorte que les données du type de M : Showable soient compatibles avec celles du module résultant de l'application Print(M), il faut le préciser explicitement via l'annotation with type t = M.t. Sans cela, le vérificateur de type se plaindra :

module Show_int = struct
  type t = int
  let show = string_of_int
end

module Print_abs : Print_abs = functor (M : Showable) -> struct
  type t = M.t
  let show = M.show
  let print x = print_string (show x)
  let println x = print_endline (show x)
end

module Print : Print = functor (M : Showable) -> struct
  type t = M.t
  let show = M.show
  let print x = print_string (show x)
  let println x = print_endline (show x)
end;;


module Print_int_abs = Print_abs (Show_int)
module Print_int = Print (Show_int)

(* incompatibilité des types *)
Print_int_abs.println 1;;
Error: This expression has type int but an expression was expected of type
Print_int_abs.t

(* types compatibles *)
Print_int.println 1;;
1
- : unit = ()

Cependant l'aspect verbeux peut, dans les faits, se limiter aux fichiers d'interface .mli et le code effectif du fichier .ml être tout simplement :

module Show_int = struct
  type t = int
  let show = string_of_int
end

module Print (M : Showable) = struct
  type t = M.t
  let show = M.show
  let print x = print_string (show x)
  let println x = print_endline (show x)
end

module Print_int = Print (Show_int)

Cela parait peut être évident pour toi qui est tombé dedans que tu es petit.

Je ne suis pas tombé dedans quand j'étais petit : c'est un niveau d'abstraction (auquel je suis largement habitué pour d'autres raisons, et encore je ne trouve pas cela très abstrait) dont j'ai ressenti le besoin, et j'ai appris la façon dont OCaml le met à disposition et à m'en servir. Si on n'en ressent pas soi même le besoin pour des raisons de généralisation, le concept de module semble tombé comme un cheveux sur la soupe.

Les modules ressemblent ici vaguement à des objets, avec des définitions de type dedans, mais avec une autre syntaxe.

Les deux syntaxes sont assez proches : ce sont les mots-clés qui changent. Cela me semble utile, voire conseiller au niveau du principe de moindre surprise, le second généralisant (en quelque sorte) le premier il serait surprenant que la syntaxe ne le signifie pas par un moyen quelconque : autrement on risquerait de confondre les deux notions.

Pour conclure ce commentaire déjà bien long, comme toutes ces questions tournent autour de la notion d'abstraction (fonction, type paramétré, objet, module, foncteur…) il est normal que le lamba-calcul soit un outil théorique de premier choix. Dans ce langage, il n'y a que deux notions fondamentales : l'abstraction (le lambda) et l'usage d'abstraction (l'application). :-)

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

En fait, je pensais au cas d'usage qui reviennent au même.

Mais s'il y a trois notations distinctes ce n'est pas pour l'espace de fonctionnalité qu'elles ont en commun, mais justement pour les fonctionnalités où elles diffèrent.

Lorsque l'on écrit :

let rp : pt_2D = {x = 1.0; y = 2.0}

let op : obj_pt_2d = object method x = 1.0 method y = 2.0 end

module MP : mod_pt_2D = struct let x = 1.0 let y = 2.0 end

il y a des situations où utiliser l'une ou l'autre ne change rien (c'est le cas de tous mes exemples, sauf le dernier qui était là pour montrer ce que seul les modules peuvent faire sans encodage tricky), mais il y a des cas d'usage que seul l'une des approche permet d'appréhender. Tout dépend des besoins du programmeur et des choix architecturaux qu'il fera pour son application. Si je veux juste un dictionnaire de valeurs, je prends un enregistrement ; si je veux un dictionnaire avec relation de sous-typage (la base du paradigme objet), je prends un objet ; si j'ai besoin d'un plus haut niveau d'abstraction et de généricité qu'offre le langage, je prends un module. Comme l'absence de généricité ne semble pas te gêner dans un langage (en 2017 pour un langage jeune, j'ai du mal à comprendre), je comprends que l'utilité des modules ne te semble pas évidente.

Je t'ai lu, plus d'une fois, disant que tu appréciais l'approche tagless-final pour l'interprétation¹ mais sans un niveau de généricité acceptable tu oublies (et sans higher-kinded polymorphism ça doit être une plaie à faire): c'est une condition sine qua non que doit offrir le langage hôte pour la mettre en pratique !

même si c'est formel

Il ne faut pas trop se prendre la tête sur cette notion de formel ou de formalisme. Toute pensée, consciemment ou inconsciemment, explicitement ou implicitement, est formelle : une pensée informelle est un non-sens, une contradiction dans les termes, un carré rond si tu préfères. Ce que font les approches formelles c'est rendre explicite le formalisme sous-jacent qui se trouve à la source de la pensée exprimer dans tel ou tel langage.

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

Par contre, ce n'est pas du tout évident en lisant tes exemples.

Essaye de faire le dernier exemple avec un enregistrement, tu verras le problème. ;-)

type ('t,'u) par = {v : 'u 't};;
Error: Syntax error

Il est possible d'encoder la chose avec des enregistrements en utilisant la bibliothèque Higher et la technique dite de défonctionnalisation de Reynolds (transformer un code fonctionnel vers un langage non fonctionnel), mais ça devient aussi tricky que les modules.

(*
 ce type sert d'encodage pour dire que l'on applique 
 le type paramétrique 't à la variable de type 'a
*)

type ('a, 't) app

module Higher_Kind (T : sig type 'a t end) =
struct
  (* on a notre type paramétrique *)
  type 'a s = 'a T.t

  (* on le manipule de l'extérieur comme un type non paramétrique *)
  type t

  (* une injection et une projection pour passer de la version
     paramétrique à son encodage non paramétrique *)
  external inj : 'a s -> ('a, t) app = "%identity"
  external proj : ('a, t) app -> 'a s = "%identity"
end

module Higher_list = Higher_Kind(struct type 'a t = 'a list end)
module Higher_option = Higher_Kind(struct type 'a t = 'a option end)

type ('t, 'u) par = {v : ('u, 't) app}

let m = {v = Higher_list.inj ["Hello World !"]};;
val m : (Higher_list.t, string) par = {v = <abstr>}

let n = {v = Higher_option.inj (Some 1)};;
val n : (Higher_option.t, int) par = {v = <abstr>}

M.v = Higher_list.proj m.v && N.v = Higher_option.proj n.v;;
- : bool = true

Manipuler les types paramétriques (qui sont des fonctions des types vers les types) comme des types de première classe au niveau des abstractions est ce que l'on appelle communément higher-kinded polymorphism : cela revient à voir le langage des types comme un langage fonctionnel et à lui associer son propre système de type (ou kind) en conséquence.

Et pourquoi 3 syntaxes différentes pour faire la même chose ou presque ?

Parce que les 3 ne font pas la même chose : les modules permettent de faire ce que font les deux autres, les objets ont l'héritage et le sous-typage mais pas les enregistrements, tous les modules ne peuvent pas être manipuler correctement en tant que citoyen de première classe (ceux qui ont des types paramétriques justement), et que le compilateur ne leur associe pas la même représentation mémoire en conséquence des différentes possibilités qu'ils offrent.

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

En Ocaml, le code de base ne me pose pas de problème, si tu joues avec les modules et leur définition et un gadt au milieu, je vais beaucoup transpirer.

Qu'est-ce qui te pose problème avec les modules ? Ce sont juste des enregistrements (tout comme les objets) avec des déclarations de type (pas comme les objets : les modules c'est des objets sous stéroïdes). Exemples :

(* un point en 2D vu comme un enregistrement *)
type pt_2D = {x : float; y :float}

(* un point en 2D vu comme un objet *)
class type obj_pt_2d = object
  method x : float
  method y : float
end

(* un point en 2D vu comme un module *)
module type mod_pt_2D = sig
  val x : float
  val y : float
end

(* une valeur pour chaque type représentant le même point *)
let rp : pt_2D = {x = 1.0; y = 2.0}
let op : obj_pt_2d = object method x = 1.0 method y = 2.0 end
module MP : mod_pt_2D = struct let x = 1.0 let y = 2.0 end

rp.x = op#x && rp.y = op#y && rp.x = MP.x && rp.y = MP.y;;
- : bool = true

Contrairement aux enregistrements, on peut étendre les objets et modules par héritage :

class type obj_pt_3D = object
  inherit obj_pt_2d
  method z : float
end

module type mod_pt_3D = sig
  include mod_pt_2D
  val z : float
end

let op_3D : obj_pt_3D = object
  method x = op#x
  method y = op#y
  method z = 3.0 
end
module MP_3D = struct include MP let z = 3.0 end

op_3D#x = MP_3D.x && op_3D#y = MP_3D.y && op_3D#z = MP_3D.z;;
- : bool = true

mais seuls les modules peuvent contenir des déclarations de type, ce qui rend le concept plus abstrait, c'est à dire plus générique. ;-)

module type Point_2D_t = sig
  (* type des coordonnées *)
  type t

  (* coordonnées du point *)
  val x : t
  val y : t
end

(* les annotations de type ne sont pas nécessaires, je les
   mets juste pour souligner qu'ils réalisent la signature *)

module Pt_float : Point_2D_t with type t = float = struct
  type t = float
  include MP
end

module Pt_int : Point_2D_t with type t = int = struct
  type t = int
  let x = 1
  let y = 2
end

On pourrait faire la même chose en utilisant un enregistrement paramétrique : généricité sur les enregistrements (avec les objets, ça marche aussi).

type 't pt_2D_t = {x : t; y : t}

let p_float : float pt_2D_t = { x = 1.0 ; y = 2.0}
let p_int : int pt_2D_t = {x = 1; y = 2}

Pt_float.x = p_float.x && Pt_float.y = p_float.y;;
- : bool = true

Pt_int.x = p_int.x && Pt_int.y = p_int.y;;
- : bool = true

Mais là où seuls les modules peuvent exprimer un tel degré de généricité, c'est lorsque le type déclaré dans le module est lui-même paramétrique.

module type Par = sig
  type 'a t
  type u
  val v : u t
end

module M : Par with type 'a t = 'a list and type u = string = struct
  type 'a t = 'a list
  type u = string
  let v = ["Hello World !"]
end

module N : Par with type 'a t = 'a option and type u = int = struct
  type 'a t = 'a option
  type u = int
  let v = Some 1
end

Les modules permettent de pousser la généricité du code à un niveau inaccessible aux enregistrements et aux objets.

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

Je n'ai pas (encore ?) lu "Le fantôme de la transparence", mais je pense que tu sautes un peu du coq (sic) à l'âne.

Oui, je saute du coq à l'âne, cette question m'est juste venue à l'esprit par association d'idée, je ne sous-entendais pas un lien fort entre les deux concepts de tests.

dans les derniers machins de Girard […]

Il y a une chose qui m'intringue chez Girard dans sa lecture de la syllogistique aristotélicienne. Il met systématiquement en rapport la forme Barbara (les animaux sont mortels, or les hommes sont des animaux, donc les hommes sont mortels) avec la transitivité de l'implication (composition des morphismes catégoriques pour la logique classique, composition des opérateurs hilbertiens pour la logique linéaire) :

(*
|- A -> B    |- B -> C
-----------------------
      |- A -> C
*)

fun g f x -> f (g x);;
- : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = <fun>

là où, pour moi, il m'apparait plus évident que Barbara c'est du sous-typage structurel :

 S <: M    M <: P
------------------
      S <: P

Barbara : c'est la transitivité du sous-typage, raison pour laquelle les prédicats sont unaires chez Aristote et qu'il n'y a aucune distinction logique entre sujet et prédicat : quelque chose qui ne peut être pensée que comme sujet mais jamais comme prédicat est une substance, concept qui appartient à la métaphysique mais non à la logique (comme un terme qui ne peut être également vu comme un type).

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

En effet le cerveau n'est pas si fort que ça en logique, même celui d'un programmeur moyen.

M'est avis que le programmeur moyen devrait s'y former un minimum, il y aurait moins de bugs dans les programmes. Les systèmes à typage statique étant en grande partie basés sur la logique formelle, ils imposent déjà, de fait, une certaine hygiène logique aux développeurs.

La logique est une science rationnelle non seulement selon la forme, mais selon la matière : une science a priori des lois nécessaires de la pensée, non pas relativement à des objets particuliers, mais bien relativement à tous les objets en général : c'est donc une science du droit usage de l'entendement et de la raison en général, non pas de façon subjective, c'est-à-dire non pas selon des principes empiriques (psychologiques) : comment l'entendement pense — mais de façon objetive, c'est-à-dire selon des principes a priori : comment il doit penser.

Kant, Logique.

Le graissage est de moi. ;-)

C'est aussi illustré par ce jeu sur Clips (langage).

Je n'ai pas bien compris ce que devait illustrer ce jeu. Si ce n'est que certains niveaux ont une morale douteuse :-P

• pour survivre dans la jungle urbaine, il faut aller au travail enivré : vous ne serez pas payer, n'aurez pas d'argent mais au moins vous resterez en vie ;

• pour épouser la femme de vos rêves, pousser votre rival dans les bras d'une psychopathe pour qu'elle le tue.

Le premier cas correspond au problème technique suivant pour un programmeur : trouver un environnement de tel sorte qu'un état possible du système ne soit jamais atteint. Le second au problème inverse : trouver un environnement pour qu'un état soit atteint.

Le jeu ayant une sémantique avec effet de bord, ce que cela montre surtout c'est qu'il n'est pas toujours évident de raisonner en présence d'effets de bord : ce dont les logiciens et les adeptes de la programmation fonctionnelle n'ont jamais douté. ;-)

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

Avant de te poser quelques questions qui me viennent en vrac, je voudrais d'abord te dire que cela fait plaisir de te lire à nouveau dans ces colonnes. :-)

Ma première question sera une question quelque peu indiscrète en réponse au pourquoi de ton journal : pourquoi avoir écrit un journal sur la question ? Autrement dit, qu'est-ce qui t'a amené à écrire là, maintenant, un article sur l'intérêt de la recherche en langages de programmation ?

La seconde m'est venue à la lecture de ce passage :

Il s'agit en quelque sorte d'un ensemble de tests pour évaluer un langage. Cet ensemble de tests évolue au fil du temps, car nous affinons notre compréhension de ces propriétés formelles et nous en proposons de nouvelles, à partir de nos expériences d'utilisation des langages existants ou expérimentaux.

As-tu lu le dernier ouvrage de Jean-Yves Girard : Le fantôme de la transparence ? Il y expose les avancées de la logique mathématique, en particulier la logique linéaire, et le rapport syntaxe-sémantique y est présenté via l'image de l'usine et de l'usage qui se testent réciproquement (son exemple fil rouge est celui du lecteur blue-ray et du blue-ray et des convertisseurs blue-ray vers dvd : un lecteur teste que l'objet est un bien blue-ray, comme le blue-ray peut tester que lecteur en est bien un).

La suivante a trait à la cohérence des langages et plus particulièrement OCaml. J'ai toujours trouvé qu'il y a un manque de cohérence dans la syntaxe concrète des types paramétriques : ce sont des fonctions des types vers les types, pourquoi ne pas utiliser la même syntaxe que les fonctions et la curryfication ? Haskell n'a pas ce défaut et ReasonML le corrige pour OCaml (c'est bien là la seule amélioration de cette syntaxe, pour le reste j'espère bien que ça ne s'étendra pas au-delà de la communauté Javascript). Ce point a-t-il déjà été abordé au sein de l'équipe en charge du développement du langage ?

Enfin, sans doute la question la plus importante : où en est le langage Chamelle ? A-t-il suivi les évolutions de son binôme soumis à l'impérialisme linguistique de la perfide Albion ? Un tel code est tout de même plus convenable pour un francophone :-D

type 'a arbre = Feuille de 'a | Nœud de 'a arbre * 'a arbre

soit rec feuille_existe p arbre =
  filtre arbre avec
  | Feuille v -> p v
  | Nœud (gauche, droite) ->
      feuille_existe p gauche
      || feuille_existe p droite

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

Mais du coup, ça ne résout rien : à la première connexion, ce n’est pas bon, et donc, il faut quand même une action pour avoir le contenu dans la bonne langue. Comparé à « cliquer sur le petit drapeau et le site s’en souvient au moyen d’un cookie », on n’a pas avancé d’un iota.

Cette solution est un hack côté client pour les serveurs qui gérerait mal l'en-tête.

Mais il a aussi toute latitude pour l’interpréter comme « je t’envoie le français quoi qu’il advienne car c’est ce que tu as mis en premier ». En fait, je pense même que c’est plutôt ce qu’il est censé faire (à qualité égale, le comportement logique est que l’ordre d’apparition prime, de la même manière que lorsque la qualité n’est pas spécifiée).

Je ne crois pas. Fais ce test chez toi :

wget --header='Accept-Language: fr,en;q=0.8' https://www.debian.org/ -O debian_fr.html
wget --header='Accept-Language: fr,en' https://www.debian.org/ -O debian_vo.html
wget --header='Accept-Language: fr;q=0.5,en;q=0.5' https://www.debian.org/ -O debian_vo2.html

Chez moi seule la première page est en français. La RFC dit que quand la qualité n'est pas précisée elle vaut 1 par défaut et des langues de même qualité se valent pour l'utilisateur. Le plus logique pour le serveur est d'envoyer la VO si elle fait partie de ces langues.

Le problème de firefox (je ne sais pas ce que font les autres) est qu'il ajoute tout seul un paramètre de qualité unique pour chaque langue, ce qui fait qu'il n'y a jamais deux langues de même valeur dans l'en-tête : elles sont ordonnées. Même si je modifie la valeur de l'en-tête manuellement via la clé intl.accept_languages pour mettre fr;q=1,en;q=1, quand je vais sur le validateur w3 il me répond que mon en-tête a la valeur Accept-Language: fr,en;q=0.5. C'est mon navigateur qui fait n'importe quoi : le problème est dans le client non dans la RFC.

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

Là c'est toi qui ne lis pas ce que j'écris.

Chaque fois qu’il visite un nouveau site, tu vas lui demander de saisir la langue dans lequel il le souhaite ?

Certainement pas, il suffit de lui laisser la possibilité de le faire s'il le souhaite, non de l'obliger à choisir pour chaque nouveau site. Tu as une option standard pour tous les sites, sauf ceux spécifier autrement. Au passage, le site MDSN a bien d'autre défaut, je n'arrive même pas à m'y connecter : « Firefox a détecté que le serveur redirige la demande pour cette adresse d’une manière qui n’aboutira pas ».

Le standard ne répond pas au cas d’utilisation.

Si il y répond : dans la RFC c'est un would non un should ou un must. Je maintiens qui si tu mets les langues française et anglaise à égalité pour le facteur de qualité, le serveur à toute latitude pour interpréter ton en-tête comme signifiant : « VO si VO=français, sinon VO si VO=anglais, sinon français, sinon anglais, sinon VO ».

Je maintiens que le problème n'est pas dans la RFC, mais dans son usage tant par les navigateurs que par les serveurs. Si les uns ou les autres sont idiots, aucune RFC ne pourra jamais résoudre leurs problèmes de communications : le problème n'est pas alors d'ordre technique.

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