kantien a écrit 1227 commentaires

Je reconnais que ma formulation n'était pas claire, et pouvait prêter à confusion. Ce que je voulais dire c'est que toute dette ne crée pas nécessairement de la monnaie, mais que certaines en créent. Ce qui importe, c'est que le porteur d'une valeur monétaire possède une reconnaissance de dette que tout un chacun est libre d'accepter en échange d'un bien ou d'un service.

Dans mon exemple fictif, la dette que B contracte envers A peut bien être à l'origine de la création de monnaie, tout comme ce pourrait déjà être un titre de dette dont il disposerait déjà. Ensuite libre à chacun d'accepter ou non cette monnaie comme véhicule de leurs échanges. Néanmoins, si cette dette crée de la monnaie et qu'ensuite B s'acquitte de la dette qu'il a envers C, alors cette quantité de monnaie est détruite. C'est le phénomène dont parlait sub0 lorsqu'il disait : « le mécanisme de création monétaire est complété par celui de destruction ».

Comment les banques créent la monnaie… quelques mythes sur le site d'un économiste québécois.

Pour l'exemple que tu me proposes : d'une il n'est pas nécessaire de faire intervenir de la monnaie pour que l'échange puisse avoir lieu s'ils possèdent déjà ce qu'ils souhaitent échanger; deuxièmement ils peuvent, dans la réalité, obtenir une reconnaissance de dette auprès d'un tiers (ou de l'un d'entre eux s'ils ne sont que tous les trois, mais c'est un univers bien fictif que tu décris) qui peut garantir, sur les biens existants en sa possession, que la dette sera honorée afin d'inspirer confiance dans la monnaie ainsi créée.

Et ce genre de système n'exclut nullement l'économie du don en se restreignant à l'économie marchande. La suite du pamphlet Maudit argent, dont j'ai donné un extrait dans un autre commentaire, contenant ceci :

Que si vous me cédez cet écu gratuitement, en ce cas, il est certain que j’en serai d’autant plus riche, mais vous en serez d’autant plus pauvre, et la fortune sociale, prise en masse, ne sera pas changée ; car cette fortune, je l’ai déjà dit, consiste en services réels, en satisfactions effectives, en choses utiles. Vous étiez créancier de la société, vous m’avez substitué à vos droits, et il importe peu à la société, qui est redevable d’un service, de le rendre à vous ou à moi. Elle s’acquitte en le rendant au porteur du titre.

Le mécanisme de création monétaire de la TRM ne reposant sur nulle garantie d'existence de services réels, de satisfactions effectives, de choses utiles, ce en quoi consiste à proprement parler la richesse, me semble, de son côté, être une monnaie de singe : c'est la planche à billet. Pour ma part, je ne voudrais ni en recevoir, ni en échanger, ni en donner.

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

Le problème pourrait donc être formulé différemment : les sites dont il est question font-ils partie de l'espace public ?, et leur contenu remet-il en cause le droit à l'avortement des femmes qui chercheraient à l'exercer ?

Il y a un problème dans cette formulation. Telle que je la comprends, j'aboutis à la conclusion qu'il devrait être interdit de remettre en cause publiquement un droit existant. On fait comment, alors, pour exprimer son désaccord envers une loi existante pour en demander l'abrogation ? Je suis opposé aux DRM, et je souhaiterais que le droit d'y avoir recours soit abrogé : je dois me taire ? Ou alors, seuls certains droits ne peuvent être remis en cause publiquement ? Soit, mais lesquels et selon quels critères ? Et de quel droit ne peut-on les remettre en cause ?

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

Cette vidéo est un fake ! Les américains n'ont jamais posé les pieds sur la lune : on en trouve plein de preuves sur le nain ternet. :-P

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

Ainsi donc, une contrat de dette, de gré à gré entre A et B, devrait donc devenir de la monnaie pour C ?

Je n'ai jamais dit qu'un contrat de dette créé de la monnaie, mais que la monnaie représentait une reconnaissance de dette. Ce qui n'est pas la même chose.

La TRM, en résolvant le problème des trois producteurs

Et l'humanité a bien entendu attendu la TRM pour résoudre ce problème et dépasser le stade du troc entre deux personnes. Non, pour cela, elle a inventé l'argent comme représentant une reconnaissance de dette et pouvant, par là, se substituer à n'importe quel bien ou service car il les représente tous. Ainsi si A rend un service à B, alors ce dernier a une dette vis à vis de A. Dans un système de pur troc de gré à gré, il doit lui même lui rendre un bien ou un service équivalent pour équilibrer leur compte. En inventant l'argent, B paye A qui peut alors aller voir C pour recevoir le service qu'on lui doit, et en donnant à C l'argent qu'il a obtenu de B, c'est maintenant B qui a une dette envers C.

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

kantien : La notion que tu décris et que tu nomme "argent" n'existe que dans les esprits de ceux qui la pense.
Dans le monde réel, les hommes n'ont que faire de ces notions. Ils échangent parce qu'ils ont besoin d'échanger. Et c'est par l'expérience des limites du troc que les hommes ont tout naturellement chercher à créer un moyen d'échange intermédiaire, qu'est la monnaie.

Je n'ai jamais soutenu le contraire. D'ailleurs, comme je suis philosophiquement kantien, cette chose que le gens appellent réalité n'existe également pour nous (je veux dire les kantiens) que dans la tête de ceux qui la pense : c'est-à-dire les hommes. Bon, ce dernier point n'est pas de grande importance pour la question qui nous occupe, c'est juste une remarque en passant.

Et c'est là ton erreur. Les hommes font d'abord des échanges, et ensuite, s'ils le souhaites, des sous-parties d'entre eux peuvent faire société, et se fixer des règles communes, c'est seulement à partir de là qu’intervient le juridique.

Et c'est la ton erreur : le juridique est antérieur à l'État, ce que tu appelles cette sous-partie des hommes qui font société et se fixent des règles communes. La thèse selon laquelle l'État crée le droit, qui lui est donc postérieur, est celle du positivisme juridique en philosophie du droit. Pour ma part, j'appartiens au courant jusnaturaliste qui soutient que les droits des hommes sont antérieurs à l'existence de l'État, et ce dernier n'a pour fonction que des les reconnaître et de les rendre effectifs là où dans l'état de nature (celui dans lequel l'on fait abstraction de l'existence d'une législation positive) ils ne sont que problématiques (il y a changement de modalité dans le jugement de droit, remarque qui s'éclaircira plus bas).

Si l'on ne voulait, avant d''entrer dans l'état civil, reconnaître comme juridique absolument aucune acquisition, même pas à titre provisoire, cet état civil serait lui-même impossible. Car, quant à la forme, les lois portant sur le mien et sur le tien, contiennent, dans l'état de nature, exactement la même chose chose que ce qu'elles prescrivent dans l'état civil, pour autant que celui-ci est conçu selon des purs concepts de la raison : simplement, dans l'état civil, se trouvent indiquées les conditions sous lesquelles ces lois parviennent à être mises en œuvre (conformément à la justice distributive). En ce sens, si, dans l'état de nature, il n'y avait pas aussi, à titre provisoire, un mien et un tien extérieurs, il n'existerait pas non plus de devoirs de droit à cet égard, et par conséquent il n'y aurait aucun commandement imposant de sortir de cet état.

Kant, Doctrine du droit.

D'ailleurs que pourraient bien échanger les hommes si ce n'est leur propriété ? Dans la notion d'échange est analytiquement contenu, en vertu du principe de contradiction, la notion de transfert réciproque de propriété. Autrement dit, les hommes s'échangent leur droit d'usage sur des choses (échanges de biens) ou l'usage de leur force (échanges de services). Ce qui ramène les échanges à de l'aliénation réciproque de droits de trois types : bien contre bien, service contre service, ou bien contre service. Ce qui fait que ton principe fondamental : « la réalité des échanges entre les hommes est d'abord mathématique, et ensuite éventuellement juridique » est notoirement erroné. Et comme je suis mathématicien et logicien de formation, j'ai un radar assez aiguisé de détection pour un usage foireux de la science mathématique. ;)

la TRM est simplement une démonstration de la forme que doit avoir une monnaie pour respecter 4 libertés économiques énoncées en axiomes […]

De mon point de vue, la TRM, que j'ai lue plus d'une fois avec attention, est un bon exemple de ce qu'il ne faut pas faire lorsque l'on prétend effectuer une démonstration mathématique.

en revanche tu ne peut pas être en désaccord avec une démonstration mathématique qui se contente d'affirmer "A implique B" et par contraposée "non B implique non A".

Effectivement, je ne serai pas en désaccord si la démonstration avait été apportée (de quoi, on ne sait pas trop d'ailleurs).

En revanche, Kant qui était logicien et philosophe, dans sa Doctrine du droit, a exposé une théorie de typage du droit romain dans la veine de ce que les logiciens-mathématiciens feront environ 150 ans plus tard avec la théorie des types du lambda-calcul et qui porte le nom de correspondance de Curry-Howard. Et vu que tu parles des jugement hypothétiques et de leur forme contraposée, ces derniers correspondent en droit aux droits personnels, ceux qui sont à l'œuvre dans le droit des contrats et les échanges de services. ;-)

In fine, ce n'est pas tant un désaccord sur ce que tu appelles les 4 axiomes des libertés économiques (que je partagent), ni peut être de la société dans laquelle l'on souhaite vivre; mais plutôt un désaccord sur ce que l'on entend par démonstration mathématique rigoureuse, voire une différence philosophique sur le concept du Droit, qui semble nous opposer.

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

je parie que tu n'as regardé aucune des vidéos que j'ai posté ni même une seule des vidéos de Heu?reka ou Stupid Economics.

J'en ai assez vu (je ne suis pas allé au bout de la totalité) pour savoir qu'il s'agit d'un propos que j'ai mainte fois lu et entendu, propos qui ne m'a absolument pas convaincu.

J'ai rien compris à ta phrase par contre : argent c'est un métal, parle de monnaie plus tôt.

Non, je parle bien de l'argent dans son acception économique et pas du métal. Ce que tu appelles des crypto-monnaies mériteraient plutôt le titre d'argent et non de monnaie. Comme j'ai la flemme d'écrire une réponse sur la distinction, je cite :

Ce que c’est que l’argent.

L’argent est une chose dont on ne peut faire usage qu’en l’aliénant. C’est là une bonne définition de mot (suivant Achenwall), c’est-à-dire une définition qui suffit à distinguer de toute autre cette espèce d’objets de l’arbitre ; mais elle ne nous éclaire nullement sur la possibilité de cette chose. Pourtant il est déjà aisé de voir : 1° que cette aliénation n’a pas pour but dans les relations une donation, mais une acquisition mutuelle (au moyen d’un pactum onerosum) ; 2° que, n’étant considéré (chez un peuple) que comme un moyen de commerce universellement agréé, mais qui n’a en soi aucune valeur, à la différence de ce qui est marchandise (c’est-à-dire de ce qui a une valeur et se rapporte au besoin particulier de l’un ou de l’autre dans le peuple), il représente toutes les marchandises.

Un boisseau de blé a directement la plus grande valeur comme moyen de satisfaire un besoin de l’homme. On peut en nourrir les animaux qui, à leur tour, servent à nous nourrir, à porter et à travailler à notre place, et concourent ainsi à la conservation et à la multiplication des hommes, lesquels non-seulement peuvent toujours obtenir de la nature de nouvelles productions, mais encore venir en aide à tous nos besoins au moyen des produits de l’art, ou nous être utiles pour la construction de nos demeures, la confection de nos habillements et, en général, pour toutes ces jouissances recherchées et toutes ces commodités qui constituent les biens de l’industrie. La valeur de l’argent au contraire n’est qu’indirecte. On ne peut en jouir directement ni l’employer immédiatement, comme tel, à quelque usage ; mais il n’en est pas moins un moyen qui est entre toutes choses de la plus haute utilité.

On peut fonder provisoirement sur ce qui précède cette définition réelle : l’argent est un moyen général pour les hommes d’échanger entre eux les produits de leur travail, de telle sorte que la richesse nationale, en tant qu’elle a été acquise au moyen de l’argent, n’est proprement que la somme du travail avec lequel les hommes se payent entre eux, et qui est représenté par l’argent en circulation dans le peuple.

La chose à laquelle peut convenir le nom d’argent doit donc avoir coûté elle-même à ceux qui l’ont produite ou procurée aux autres hommes, un travail équivalent à celui qu’a coûté la marchandise (les produits de la nature ou de l’art) et contre lequel on l’échange. En effet, s’il était plus facile de se procurer la matière nommée argent que la marchandise, il y aurait sur le marché plus d’argent que de marchandise ; et, comme le marchand aurait dépensé plus de travail pour se procurer sa marchandise que l’acheteur pour se procurer son argent, qui lui viendrait vite et en abondance, le travail que nécessite la confection des marchandises et l’industrie en général, ainsi que l’activité commerciale, source de la richesse publique, décroîtraient et dépériraient rapidement. — Aussi les billets de banque et les assignats ne peuvent-ils être considérés comme de l’argent, quoiqu’ils en tiennent lieu pendant un temps ; ils ne coûtent presque aucun travail, et leur valeur se fonde uniquement sur cette opinion que l’on pourra continuer de les échanger contre de l’argent comptant. Dès qu’on s’aperçoit que l’argent n’est pas en quantité suffisante pour un échange facile et sûr, cette opinion, s’évanouissant tout à coup, rend inévitable la perte du remboursement. Ainsi le travail de ceux qui exploitent les mines d’or et d’argent au Pérou ou au Nouveau-Mexique, surtout si l’on songe à toutes les tentatives malheureuses et à toutes les peines inutiles que coûte la recherche des veines métalliques, est vraisemblablement plus considérable que celui qu’exige la confection des marchandises en Europe ; et, n’étant plus payé, par conséquent tombant de lui-même, il aurait bientôt réduit ces pays à la misère, si, de son côté, l’industrie de l’Europe, excitée précisément par l’appât de ces matières, ne s’était développée proportionnellement, de manière à entretenir chez eux, par les objets de luxe qu’elle leur offrait, le goût de l’exploitation des mines. C’est ainsi que toujours le travail suscite la concurrence du travail.

Mais comment est-il possible que ce qui était d’abord marchandise soit devenu à la fin de l’argent ? Cela arrive lorsque le souverain d’un pays faisant une grande consommation d’une matière qui ne servait d’abord qu’à l’ornement et à l’éclat de ses serviteurs ou de sa cour (par exemple l’or, l’argent, le cuivre ou cette espèce de beaux coquillages appelés cauris, ou encore, comme dans le Congo, une espèce de nattes nommées makate, ou, comme dans le Sénégal, des lingots de fer, ou même, comme sur les côtes de la Guinée, des esclaves nègres), lorsque, dis-je, ce souverain exige que ses sujets lui payent certains impôts en cette matière (comme marchandise), et qu’à son tour, les poussant ainsi à travailler pour la fournir, il les paye avec la même matière, d’après les lois du commerce qui s’établit entre eux et avec eux en général (sur un marché ou dans une bourse). — C’est de cette manière seulement (selon moi) qu’une marchandise a pu fournir aux sujets un moyen légal d’échanger entre eux les produits de leur travail, et par là aussi une source de richesse nationale, c’est-à-dire de l’argent.

Le concept intellectuel, auquel est subordonné le concept empirique de l’argent, est donc celui d’une chose qui, comprise dans la circulation de la possession (permutatio publica), détermine le prix de toutes les autres choses (de toutes les marchandises), parmi lesquelles il faut compter même les sciences, en tant qu’on ne les enseigne pas gratuitement aux autres. L’abondance de l’argent chez un peuple constitue son opulence (opulentia). Car le prix (pretium) est le jugement public porté sur la valeur (valor) d’une chose, relativement à la quantité proportionnée de ce qui est le moyen universel et représentatif de l’échange réciproque des produits du travail (de la circulation). C’est pourquoi, là où le commerce est grand, ni l’or ni le cuivre ne sont considérés proprement comme monnaie, mais seulement comme marchandise, parce qu’il y a trop peu de l’un et trop de l’autre pour qu’on puisse les mettre aisément en circulation et les avoir en même temps en aussi petites parties qu’il est nécessaire pour les échanger contre des marchandises dans les plus petites acquisitions. Le métal d’argent (plus ou moins allié de cuivre) est donc regardé dans le grand commerce du monde comme la matière propre de la monnaie, et comme la mesure qui doit servir à calculer tous les produits. Les autres métaux (à plus forte raison les matières non métalliques) ne peuvent avoir cours que chez un peuple qui fait peu de commerce. Les deux premiers, quand ils ne sont pas seulement pesés, mais encore estampés, c’est-à-dire marqués d’un signe qui en indique la valeur, sont de l’argent légal, c’est-à-dire de la monnaie.

« L’argent est donc (suivant Adam Smith) un corps dont l’échange est le moyen et en même temps la mesure de l’activité avec laquelle les hommes et les peuples font le commerce entre eux. » — Cette définition ramène le concept empirique de l’argent à un concept intellectuel, en ne considérant que la forme des prestations réciproques dans le contrat onéreux (et en faisant abstraction de leur matière), c’est-à-dire en ne considérant que le concept du droit dans l’échange du mien et du tien en général (commutatio late sic dicta), afin de représenter convenablement le précédent tableau d’une division dogmatique à priori, par conséquent du système de la métaphysique du droit.

Emmanuel Kant, Doctrine du Droit

Le graissage sur le fin du texte est de moi, il est là pour souligner que la définition du concept est avant tout juridique. Ne pas aborder correctement cette définition, avant de vouloir traiter mathématiquement la notion (comme l'a fait l'auteur de la TRM, ou Théorie Relative de la Monnaie) est une erreur qui aboutit à perpétuer les inepties sur le sujet.

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

Attention, l'histoire du Canard c'est pas tout à fait ça, c'est même l'inverse en fait.

Merci pour ce rappel historique, ma mémoire m'a joué un tour sur le coup. Je croyais me souvenir que la polémique tournait autour de la chute dans le vide, et non sur l'effet de la résistance de l'air qui n'est pas identique selon la forme et la masse des corps.

Toutes mes excuses au Canard.

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

Tu sais que tout le monde n'a pas un salaire dépassant les 1500 balles par mois ?

Tout comme moi qui suis sans emploi, mais je ne vois toujours pas en quoi cela constitue un argument qui infirme ce qu'est l'argent : une reconnaissance de dette. ;-)

Sous prétexte qu'il existe des personnes sans emplois ou à faibles revenus, on devrait mettre en pratique une théorie ubuesque sur la nature de l'argent ? Tu as lu au moins le texte dont j'ai donné le lien et seulement cité un passage, ou tu fais comme d'autres commentateurs du site : tu ne lis rien, mais tu veux quand même donner ton avis ? Comme la TRM¹ fait usage (somme toute douteux) des outils de la géométrie différentielle en s'inspirant de la relativité générale, je propose le principe suivant : du fait de l'existence de personnes se trouvant dans une situation financière compliquée, je décrète, unilatéralement, que le champ de gravitation n'a aucune incidence sur la marche des horloges ! :-)

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

Car le type à l'origine de la création monétaire n'est pas endetté?

Et donc il crée du vent : c'est une magnifique bulle inflationniste ne reposant sur rien votre système !

Je constate que tu as toujours une conception bien étrange de ce qu'est l'argent (tout comme l'auteur de la TRM d'ailleurs) :

Vous avez un écu. Que signifie-t-il en vos mains ? Il y est comme le témoin et la preuve que vous avez, à une époque quelconque, exécuté un travail, dont, au lieu de profiter, vous avez fait jouir la société, en la personne de votre client. Cet écu témoigne que vous avez rendu un service à la société, et, de plus, il en constate la valeur. Il témoigne, en outre, que vous n’avez pas encore retiré de la société un service réel équivalent, comme c’était votre droit. Pour vous mettre à même de l’exercer, quand et comme il vous plaira, la société, par les mains de votre client, vous a donné une reconnaissance, un titre, un bon de la République, un jeton, un écu enfin, qui ne diffère des titres fiduciaires qu’en ce qu’il porte sa valeur en lui-même, et si vous savez lire, avec les yeux de l’esprit, les inscriptions dont il est chargé, vous déchiffrerez distinctement ces mots : « Rendez au porteur un service équivalent à celui qu’il a rendu à la société, valeur reçue constatée, prouvée et mesurée par celle qui est en moi-même. »

Frédéric Bastiat, Maudit Argent

L'argent, c'est de la reconnaissance de dette. ;-)

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

Il manque deux liens dans le corps de la dépêche (les balises [] autour des mots sont présentes mais pas le lien qui va avec) :

• celui vers le site de weblate
• un vers l'ouvrage Community Building On The Web, Secret Strategies for Successful Online Communities de Amy Jo Kim, que l'on peut demander via researchgate.

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

Maintenant, je pense que tout cela n'invalide en rien ma conclusion, qui est qu'il faut faire attention avec certaines supposition et que on peut se planter facilement.

En Coq t'aurais pas eu ce problème ! :-P Son système de type, qui est le plus riche que l'on puisse conférer au lambda-calcul, n'autorise pas de telles ambiguïtés.

Sinon pour gérer le maximum, et encoder des preuves sur ce dernier via des termes, avec les GADT il y a un bon exemple dans cette leçon sur les GADT dans le cours de programmation fonctionnelle avancée de Jeremy Yallop et Leo White. Cela rejoint ta question sur les GADT et type families dans mon journal sur la méthode tagless-final.

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

Pour être plus précis, au sens strict, ce que tu as défini sur tes structures de données n'est pas une relation d'ordre totale (on ne dit pas absolue, mais totale pour exprimer que deux éléments quelconques sont nécessairement en relation, ce qui a bien été rappelé dans un autre commentaire), mais une relation de préordre. La différence est importante, et ça a de l'impact pour ton code et tes exemples, une relation d'ordre est antisymétrique : si x <= y et y <= x alors x = y. Ce qui n'est pas le cas de ta relation : elle est symétrique (x <= x pout tout x) et transitive (si x <= y et y <= z alors x <= z) ce qui en fait une relation de préordre (symétrie et transitivité constitue la définition d'un préordre) mais non une relation d'ordre.

Ensuite quand on a une relation de préordre sur une structure, on peut définir un relation d'équivalence par x ~ y si et seulement si x <= y et y <= x. Puis à partir de ces deux relations, on définit naturellement une relation d'ordre sur les classes d'équivalence. Ton problème devient alors le suivant : quel représentant de chaque classe doivent renvoyer les fonctions min et max ? Ici il n'y a pas de réponse unique, bien que la solution choisie par Haskell ou Rust soit la plus « sensée » si l'on cherche à garantir certains invariants lorsque l'on compose des opérations faisant usage de ces différentes relations.

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

Les erreurs semblent bien avoir été corrigées. Au moins pour celle sur la signature du la fonction main d'après le manuel datant du 30 juin 2016 :

The following limitations apply to the C source files that can be interpreted.

1. […]
2. […]
3. The main function must be declared with one of the two types allowed by the C standards, namely:

int main(void) { ... }
int main(int argc, char ** argv) { ... }

Par contre, je ne comprends pas ce que tu entends par réaliste lorsque tu dis : « je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes ». Que l'on se demande si les spécifications d'un langage sont correctes et complètes (ou plutôt leur formalisation dans un autre langage), je peux le comprendre (et il n'est pas possible de le prouver formellement non plus, la question ne portant pas sur la forme mais sur la matière ou le contenu). Mais se demander si elles sont réalistes n'a aucun sens.

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

Ok, merci pour l'explication, c'est plus clair maintenant.
Une autre question : peut-on avoir plusieurs clefs associées à la même adresse ? Si oui, quelle utilité ?

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

Merci pour ce journal riche en information. N'étant pas utilisateur du système certains points m'échappent encore, mais j'en ai déjà une meilleure compréhension grâce au journal.

J'ai une question sur la politique ask du modèle TOFU : comment l'active-t-on ? Tu dis que les seules politiques par défaut possibles sont unknowkn, auto ou good; mais alors à quoi sert la politique ask ?

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

Pour la résistance, j'ai eu un peu de mal à voir la meilleur analogie : c'est une voix plus "étroite" ? il faut plus de tension pour faire passer plus de courant ?

La meilleure analogie ne serait-elle pas sa propre définition : un frottement ? Il me semble bien que la loi U = R . I n'est que la forme intégrale d'une loi différentielle qui exprime le frottement que subit la charge en traversant le conducteur. Pour l'analogie avec l'intensité du courant comme débit (la vitesse de déplacement des charges dans le milieu) par rapport à la gravitation : prendre une bille de plomb est la lâcher dans l'air, puis comparer avec la même expérience où elle doit traverser un milieu visqueux comme de la confiture. Dans la seconde elle ira moins vite, l'intensité est plus faible bien que la tension soit la même (même hauteur de chute, même différence de potentiel gravitationnel) car la résistance du milieu est plus grande.

Après avec la gravitation, il y a ce résultat marrant : en l'absence de frottement (dans le vide) une plume de 1g et un poids de 1kg tombe au sol en même temps si on les lâche de la même hauteur avec la même impulsion. Résultat bien connu depuis Galilée, qui est le point de départ de la théorie de la gravitation d'Einstein, mais que la plupart des personnes ont du mal à accepter. Je me souviens d'une série d'articles du Canard Enchaîné où les auteurs s'évertuaient à vouloir prouver le contraire, sans jamais réussir à comprendre qu'ils expérimentaient la résistance de l'air et non une propriété physique du champ de gravitation.

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

Effectivement, la coquille se trouve dans l'article d'origine de Gérard Berry, je n'ai pas relu attentivement la phrase (sachant ce qu'elle cherchait à exprimer) en citant. Mais c'est une bonne chose au final, cela illustre une source potentielle de bug dans la démarche : lorsque l'humain traduit formellement la spécification du langage. Ce qui minimise grandement la surface. Il suffit de lire les deux articles cités dans ce commentaire : 4 erreurs minimes trouvées et corrigées pour CompCert face à des centaines, non toutes corrigées, pour GCC et LLVM. :-)

Pour la note de modérateur à rajouter sur la correction, je ne sais si elle est vraiment nécessaire. Quoi que la source a une clause ND : un correction de coquille est-elle une œuvre dérivée ? :-P

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

Ces dernières années, différents bugs ont été trouvés dans CompCert par test aléatoire (PLDI'11, ISSTA'15, peut-être d'autres, je ne suis pas expert), vraisemblablement causés par des "trous" dans la spécification.

Effectivement, mais cela a été corrigé. Je ne suis pas rentré dans les détails dans le journal, mais Gérard Berry en parle dans sa présentation dont le lien est dans le journal (il y parle aussi du projet deepspec) :

L’importance de CompCert devient claire quand on regarde d’autres projets comme l’outil Csmith développé à l’université d’Utah, qui, à l’aide de techniques de génération aléatoire, a permis d’engendrer automatiquement un million de programmes C destinés à casser les compilateurs. Le résultat a été étonnant : Csmith a permis de détecter des centaines de bugs dans les principaux compilateurs C, mais aucun dans CompCert (en fait deux au début, mais pas dans les parties bien définies de C, et ces bugs ont ensuite été corrigés).

En ce qui concerne les approches formelles :

On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité.

Cette remarque s'applique inéluctablement à la conception de matériel qui repose sur des théories physiques qui sont une modélisation de la réalité. Comment prouver que le modèle « correspond » au réel ? Et d'ailleurs quel sens pourrait bien avoir une telle question ?

Pour ce qui est de la formalisation de processus de calcul, ce n'est pas le cas. Mais on peut tomber sur d'autres problématiques ironiquement bien formulées dans cet article :

1973 - Robin Milner creates ML, a language based on the M&M type theory. ML begets SML which has a formally specified semantics. When asked for a formal semantics of the formal semantics Milner's head explodes.

Robin Milner est un des pères fondateurs de la discipline dans laquelle travaille Xavier Leroy : la preuve mathématique assistée par ordinateur. Le langage OCaml est un langage de la famille ML, et tous les langages de cette famille (avec SML, OCaml, Haskell, Coq, Idris…) sont tous fondés sur la correspondance de Curry-Howard ou correspondance preuve-programme : un programme est une preuve d'un théorème mathématique et son type est l'énoncé du théorème.

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

Je vais essayer de présenter la chose autrement, avec le langage de base sur les entiers :

module type SYM_INT = sig
  type 'a repr
  type 'a obs

  val lit : int -> int repr
  val add : int repr -> int repr -> int repr
  val mul : int repr -> int repr -> int repr

  val observe : 'a repr -> 'a obs
end

Maintenant, si je définis un terme du langage via un foncteur paramétré par une interprétation, j'obtiens cela :

module T (I : SYM_INT) = struct
  open I
  let t = mul (add (lit 1) (lit 2)) (add (lit 3) (lit 4))
end;;
module T : functor (I : SYM_INT) -> sig val t : int I.repr end

En donnant une interprétation au foncteur, on obtient un terme de type int I.repr. On voit déjà comment la combinaison de la signature et du système de type de OCaml donne un type correcte à notre terme. La signature, d'une certaine façon, exprime les règles de typage de notre langage.

Ensuite, je ne sais si mon image est adaptée mais elle peut aider, on peut voir un module d'interprétation (qui implémente cette signature) comme un VM pour ce langage. Le foncteur T permet d'écrire un code, un programme, dans ce langage via le terme t. Puis lorsqu'on lui donne une VM, il exécute le programme et on obtient à l'arrivée le résultat t pour cette VM.

Dans cette façon de voir, on pourrait regarder les foncteurs d'optimisations comme un processus construisant une VM à partir d'une autre VM tout en préservant des invariants de la « sémantique » du langage.

Pour ta dernière remarque :

la génération est "refaite" à chaque type d’interprétation (eval ou pretty print)

J'ai envie de dire : comme avec l'approche par ADT ou GADT. Dans celles-ci, un programme est représenté par une structure de données (et non par un foncteur) et la génération d'une interprétation est refaite à chaque fois que l'on fait un fold dessus.

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

Je ne sais pas trop, je ne suis que le messager et je ne connais pas les entrailles du système. Sur le site du projet, à la page consacrée à son fonctionnement, on peut y lire :

The subset of C supported

CompCert C supports all of ISO C 99, with the following exceptions:

• switch statements must be structured as in MISRA-C; unstructured "switch", as in Duff's device, is not supported.
• longjmp and setjmp are not guaranteed to work.
• Variable-length array types are not supported.

Consequently, CompCert supports all of the MISRA-C 2004 subset of C, plus many features excluded by MISRA (such as recursive functions and dynamic heap memory allocation).

Several extensions to ISO C 99 are supported:

• The _Alignof operator and the _Alignas attribute from ISO C2011.
• Pragmas and attributes to control alignment and section placement of global variables.

Je pense que cela parlera plus aux développeurs C qu'à moi-même. Et pour l'architecture, on trouve ce schéma :

De ce que j'ai compris, la certification commence après la traduction en Clight.

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

Je ne suis pas certain de comprendre tes questions.

Est-ce le "code" est dupliqué pour chaque functor ?

Un foncteur c'est une fonction qui prend des modules comme paramètres et qui renvoie un module (qui pourrait lui-même être un foncteur d'ailleurs). Le système des modules avec ses foncteurs est au fond un langage fonctionnel mais non turing-complet, il est proche du lambda-calcul simplement typé (en). Qu'entends-tu par le code dupliqué pour chaque foncteur ? Il y aura de l'allocation à chaque application du foncteur, mais tout comme avec n'importe quelle application de fonction. Par exemple :

let f i = i + 1

let i = f 1
let j = f 2

ici, à chaque fois que l'on applique f on alloue de la mémoire pour stocker le résultat dans i et j. C'est pareil avec les foncteurs.

Mais dans le cas de "génération" d'une expression par lecture d'un fichier par exemple, il faut le faire pour chaque functor ?

Une expression c'est un terme d'un langage. Pour pouvoir l'interpréter, il faut le mettre dans un foncteur paramétré par un module d'interprétation, et en appliquant le foncteur tu obtiendras l'interprétation de ton choix.

Comment partager une expression qui n'est pas statique ?

Via la directive include. Par exemple si tu as un terme t, tu peux faire :

module T(I : SYM) = struct
  let t = (* la désérialisation de ton terme *)
end

Et si tu veux l'utiliser avec un autre terme t', tu fais :

module T' (I : SYM) = struct
  include T(I)
  let t' = (* expression qui comporte t *)
end

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

Je dois avouer que je n'ai jamais creusé la question. Mais les premières questions qui me viennent à l'esprit sont : comment le mot-clé where était-il géré avant sa disparition ? comment font-ils en Haskell ?

Ensuite pour ce qui relève de son intérêt et de son utilité : la construction est certes redondante avec la forme let res = let x = e1 in e2, mais d'un autre côté écrire let res = e2 where e2 = e3 permet de comprendre au premier coup d'œil où l'on veut en venir. C'est du même acabit que lorsque dans mon journal j'ai traité la question du pretty printing. En commençant par écrire la conclusion à laquelle je voulais arriver, il me semble plus simple de comprendre le développement qui s'ensuit. Tandis que si je n'avais pas procédé ainsi, le lecteur se serait sans doute demandé où je voulais en venir. C'est souvent ce qui m'arrive avec la forme let ... in lorsqu'elle sert à définir des termes auxiliaires : une fois arrivée à la fin, je dois reprendre la lecture pour comprendre.

Pour ce qui est de la gestion de la précédence : pourquoi ne pas mettre les let et where au même niveau et les voir comme une parenthèse ouvrante pour le premier et une parenthèse fermante pour le second ? Cela ne marche pas ? N'est-ce pas ce que tu as fait dans ton extension de syntaxe ?

Pour les cas que tu proposes, je les lis ainsi :

let x = y + 1 in 2 * x where y = 3
(* devient *)
let y = 3 in let x = y + 1 in 2 * x

let x1 = x2 + x3 where x2 = 1 and x3 = 2 in 2 * x1
(* devient *)
let x2 = 1 and x3 = 2 in let x1 = x2 + x3 in 2 * x1

Une petite précision terminologique : j'ai tendance à qualifier de syntaxique ce genre de problématique, et de réserver le qualificatif grammatical pour ce qui relève des problématiques de typage. Pour comparer avec le domaine de la physique, l'équation P = U * I² est syntaxiquement correcte mais grammaticalement erronée car il n'est pas possible d'unifier le deux membres de l'équation : ils n'ont pas la même unité de mesure; ce qui en fait une proposition vide de sens.

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

Merci pour ton commentaire.

L'inconvénient bien sûr, c'est que le résultat est très long, trop long je pense pour que quelqu'un qui découvre puisse confortablement le lire en une seule fois. Il faut espérer que les gens ont la discipline de faire des pauses et de reprendre la suite un autre jour, même si la structure ne l'encourage pas forcément.

Effectivement, l'article est long et dense. Il faudra y revenir plus d'une fois pour les lecteurs qui voudraient le comprendre. Et encore, j'ai fait des coupes : au départ j'abordais la problématique de l'héritage multiple par exemple. J'ai hésité, également, à le couper en plusieurs journaux mais j'ai finalement choisi cette forme en me disant que le lecteur le lirai plus d'une fois.

As-tu envisagé de le convertir en un tutoriel sur Zeste de Savoir ? C'est un site avec de bonnes valeurs d'ouverture et de diffusion de la connaisance, une équipe sympathique, et plus adaptée au stockage à long terme des connaissances que les journaux de LinuxFR, il me semble.

Je ne connaissais pas, j'y réfléchirai. Pour un tutoriel comme celui-ci, c'est sans doute une bonne idée.

Quand tu dis que le typage des GADTs n'est pas "décidable", tu veux dire qu'il n'est pas "inférable": c'est le fait de deviner le type qui n'est pas décidable, pas le fait de vérifier qu'un type donné est correct (qui est ce qu'on entend par "typage décidable").

Effectivement je me suis mal exprimé, je voulais bien dire que c'est l'inférence qui est indécidable dans le cas général pour les GADT. Vérifier la correction d'une preuve, c'est toujours décidable. Trouver une preuve, en revanche… ;-)

Un pointeur complémentaire sur les GADTs, francophone, serait le cours de Programmation Fonctionnelle Avancée de Roberto di Cosmo (ou des autres enseignants ayant donné le même cours à Paris 7).

Merci pour la référence, je n'y avais pas pensé. Pourtant je me suis rendu plus d'une fois sur le site de Roberto Di Cosmo.

Au passage, une question qui n'a rien à voir avec le thème du journal. Sais-tu pourquoi les where statement ont disparu du langage OCaml ? Je pense à cela car dans le cours de Paris 7, il y a une leçon sur les zipper, et dans son article sur le sujet Gérard Huet en faisait usage. Je trouve cette perte dommage, cela permet d'écrire des codes plus élégants, et la beauté dans le code c'est important ! Comme il répondait dans un interview, sur le blog de la SIF (Société Informatique de France), intitulée Poésie et esthétisme du logiciel :

— Binaire : […] Mais tu as dépassé l’état de le compréhension. Tu nous parles d’esthétique : un programme informatique peut-il être beau ?

—Gérard Huet : Bien sûr. Son rôle est d’abord d’exposer la beauté de l’algorithme sous-jacent. L’esthétique, c’est plus important qu’il n’y paraît. Elle a des motivations pratiques, concrètes. D’abord, les programmes les plus beaux sont souvent les plus efficaces. Ils vont à l’essentiel sans perdre du temps dans des détails, des circonvolutions inutiles. Et puis un système informatique est un objet parfois très gros qui finit par avoir sa propre vie. Les programmeurs vont et viennent. Le système continue d’être utilisé. La beauté, la lisibilité des programmes est essentielle pour transmettre les connaissances qui s’accumulent dans ces programmes d’une génération de programmeurs à l’autre qui ont comme mission de pérenniser le fonctionnement du système.

Pour les programmes, de même que pour les preuves, il ne faut jamais se satisfaire du premier jet. On est content quand ça marche, bien sûr, mais c’est à ce moment là que le travail intéressant commence, qu’on regarde comment nettoyer, réorganiser le programme, et c’est souvent dans ce travail qu’on découvre les bonnes notions. On peut avoir à le réécrire tout ou en partie, l’améliorer, le rendre plus beau.

Et je suis bien d'accord avec lui : un théorème vrai, c'est important. Mais une belle démonstration l'est tout autant ! Elle permet de mieux saisir les raisons profondes de la vérité du résultat et d'éclairer son harmonie sous-jacente.

On est accoutumé à nommer beauté les propriétés évoquées des figures géométriques aussi bien que des nombres […] C'est bien plutôt une démonstration de telles propriétés que l'on serait en droit de nommer belle, parce que, par son intermédiaire, l'entendement comme pouvoir des concepts et l'imagination comme pouvoir de leur présentation a priori se sentent renforcés (ce qui, combiné avec la précision que donne la raison, se nomme l'élégance de la démonstration); car, en tout ceci, du moins la satisfaction, bien que le fondement s'en trouve dans des concepts, est-elle subjective, tandis que la perfection implique une satisfaction objective.

Kant, Critique de la faculté de juger.

Et comme les programmes sont des preuves. :-)

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

Avant tout je voudrais te remercier pour ce super journal, instructif et très pédagogique (ce qui a certainement demandé beaucoup de temps de ta part).

De rien. Cela m'a demandé effectivement du temps, mais il me fut avant tout profitable à moi même. En vertu du principe : « ce qui se conçoit bien, s'explique bien », il me fallait d'abord bien comprendre la méthode pour pouvoir l'expliquer. Ensuite, s'il peut être utile aux lecteurs du site : c'est du bonus, et c'est pour cela que je partage ma compréhension de la technique.

Une modeste contribution pour la curryfication (il faut voir si c'est instructif ou non).

Ton explication est tout à fait correcte, et elle code un principe général de curryfication pour des fonctions sur des couples. Elle explicite un isomorphisme (du moins un des sens) entre les fonction sur des couples et leurs versions curryfiées. C'est au fond ce que l'on fait en mathématique lorsque l'on pratique des applications partielles sur des fonctions de deux variables en en fixant une et en faisant varier la seconde.

Après j'ai choisi l'approche de comparaison avec python pour ne pas trop rentrer dans des détails formels sur le principe de la curryfication. Ce passage était surtout là pour montrer qu'en rendant le contexte explicite, via la curryfication, alors on pouvait se ramener au cas d'un fold ce qui est nécessaire pour utiliser la technique tagless final. Cette question avait amené de long échanges entre toi et Nicolas Boulay dans ton journal, c'est pour cela que je voulais la traiter. D'autant que j'avais besoin du code obtenu pour la suite du journal. L'exemple du pretty printing est d'ailleurs emprunté à la vidéo de ton journal. ;-)

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

Oui, un fichier pour chaque exemple, bien séparer. Pour pouvoir comparer les évolutions et les différences. Genre je suis bloqué sur le fold appliquée aux parenthèses, mais je bloque surtout sur le principe de précédence, plus que sur le code.

Je vais voir ce que je peux faire pour mettre du code plus détaillé et commenté sur github. Je ne te promets rien, cela dépendra de mon temps libre.

Pour le principe de précédence qu'est-ce qui te pose problème ? On a d'abord une fonction de mise entre parenthèse sous condition :

let cparen b = if b then paren else (fun s -> s);;
val cparen : bool -> string -> string = <fun>

Elle permet de retourner une fonction de type string -> string selon la valeur du booléen : soit cette fonction met des parenthèses si b = true, sinon c'est l'identité et on ne met pas de parenthèses. Ensuite pour le cas de l'addition, on a :

let add x y = fun p -> cparen (p > 3) @@ show_add (x 3) (y 4)

Autrement dit, tant que la priorité du contexte est ≤ 3 on ne met pas de parenthèse : 3 représente le degré de priorité de l'opérateur additif. Ensuite comme l'addition est associative à gauche, pour le membre de gauche on reste au degré 3 de l'addition, par contre pour le membre de droite on passe au degré suivant. C'est pour distinguer 1 + 2 + 3 == ((1 + 2) + 3) de 1 + (2 + 3) == (1 + (2 + 3)). Pour la multiplication, son degré de priorité est de 4 : la multiplication est prioritaire sur l'addition.

Cela étant, c'est plus un code « standard » pour gérer la priorité des opérateurs en programmation fonctionnelle. Si tu ne vois pas trop pourquoi il fait ce qu'on lui demande, ce n'est pas très important pour le reste du journal.

Mais pourquoi ?! En objet, c'est simplement une injection. Un composant d'un objet qui est construit à l’extérieur de celui-ci et donné en paramètre au constructeur. En quoi instancier un module en fixant un des type paramètre en fait une fonction ?

J'ai du mal à comprendre où tu veux en venir, et je me suis peut être mal exprimé. Les implémentations de la signature d'un langage corresponde aux différentes interprétations du dit langage. Les foncteurs eux servent à écrire du code dans ses langages (comme les foncteurs d'exemples) ou à transformer les dits programmes (comme les optimiseurs). Pour moi, et comme l'a dit Thomas Douillard, c'est exactement le niveau d'abstraction qu'il me faut pour raisonner sur ce genre de problématique.

Depuis que j'ai découvert cette méthode, et également suite aux discussions sur le journal de présentation de MetaOCaml, il y a deux comics xkcd qui résument bien mon état du moment :

et celui-ci :

J'ai essayé d'éviter le plus possible le recours au vocabulaire et aux concepts abstraits des mathématiques, mais ce n'est pas toujours évident.

Pour ce qui est de l'approche final avec les objets de OCaml cela pourrait ressemblait au code suivant :

(* on définit la symantique d'un langage avec litéraux
 * et addition comme un type d'objet paramétré par son interprétation *)
class type ['repr] symAdd = object
  method lit : int -> 'repr
  method add : 'repr -> 'repr
end

(* là on a des fonctions pour créer nos termes
 * du langage à partir de ses implémentations *)
let lit n = fun ro -> ro#lit n
let add x y = fun ro -> ro#add (x ro) (y ro)

(* un terme d'exemple *)
let t1 () = add (lit 1) (add (lit 2) (lit 3))

(* on implémente deux interprétations *)
class eval = object
  method lit n = (n:int)
  method add x y = x + y
end

class view = object
  method lit n = string_of_int n
  method add x y = "(" ^ x ^ " + " ^ y ^ ")"
end

(* on instancie un objet pour chacune *)
let eval = new eval
let view = new view

(* notre exemple est une fonction qui prend une
 * instance de classe, à la manière d'un foncteur *)
t1 () eval;;
- : int = 6

t1 () view;;
- : string = "(1 + (2 + 3))"

Et pour étendre les langages, par exemple en rajoutant la multiplication, on fait de l'héritage entre objets :

(* on ajoute un opérateur aux langages *)
class type ['repr] symMul = object
  method mul : 'repr -> 'repr -> 'repr
end

(* la nouvelle fonction pour écrire nos termes *)
let mul x y = fun ro -> ro#mul (x ro) (y ro)

(* on étend par héritage nos précédents interprètes *)
class evalM = object
  inherit eval
  method mul x y = x * y
end

class viewM = object
  inherit view
  method mul x y = "(" ^ x ^ " * " ^  y ^ ")"
end

(* on les instancie *)
let evalM = new evalM
let viewM = new viewM

(* un exemple de test *)
let t2 () = mul (add (lit 1) (lit 2)) (add (lit 3) (lit 4))

t2 () evalM;;
- : int = 21

t2 () viewM;;
- : string = "((1 + 2) * (3 + 4))"

Cette façon de faire est plus proche de l'encodage en Haskell via les typeclasses.

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