kantien a écrit 1131 commentaires

Est-ce que tu as eu d'autres éléments dans ta vie au même moment qui auraient pu avoir un lien avec tes délires ?

Non, pas particulièrement. Un ami a eu des conséquences similaires : un délire mystique avec une statue de la vierge qui lui parlait, et il a vécu cinq jours nus dans les bois en cherchant à fuir un bûcheron imaginaire.

Pendant mes délires, j'ai fait un séjour dans un centre de repos et mon compagnon de chambre, qui était un croyant musulman, voyait l'ange Gabriel lui apparaître pour lui parler.

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

Franchement ça fait peur :|

Sur le moment, surtout pour l'entourage. Je me souviens encore de la tête de ma mère quand je lui ai demandé un couteau, afin de me le planter dans le cœur, pour lui prouver que j'étais immortel. :-/

Pour les petites crises de parano, j'en avais déjà eu, comme la plupart des fumeurs que je connais, mais de très courte durée. Là c'était plus comme dans le film « un homme d'exception », sur la vie de John Nash, lorsqu'il se met à voir des messages chiffrés dans les journaux : quand j'ai vu le film, ça m'a rappelé cette période. Parce que non seulement j'étais persuadé que les gens autour de moi parlaient en langage codé, mais je voyais aussi cela dans les journaux et à la télé. :-/

Mon psy de l'époque s'est appuyé sur mon rationalisme cartésien, et mon esprit critique, pour me faire démonter mes délires et me ramener à la raison. Ça a pris un peu de temps.

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

Comment peut-on continuer à consommer un produit, sans dépendance physique, dont on ne supporte pas les effets ?

On ne continue pas, c'est pour cela que j'ai arrêté. Mais les effets dont j'ai parlé se sont déclenchés subitement au bout de cinq années de consommations régulières, dont trois années à un rythme quotidien.

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

J’ai une amie qui a arrêté de fumer du cannabis au bout de quelques années car elle se sentait mal à l’aise, elle avait l’impression de se renfermer sur elle-même et ce depuis la première fois qu’elle en avait pris, elle a juste mis du temps à faire le rapprochement…

J'ai eu de mauvaises expériences avec ce produit, mais à l'époque j'étais un gros consommateur. J'ai fini par avoir des bouffées délirantes et des obsessions paranoïaques : j'ai voulu prouver à mes proches que j'étais devenu immortel et que la seule solution pour me tuer était de me couper la tête (il ne doit en rester qu'un !); ou bien toutes les conversations tournaient autour de moi mais les personnes utilisaient un langage codé pour que je ne comprenne pas (mon entourage devenait fou, ils ne pouvaient plus rien dire). Ça a duré plusieurs mois, et depuis je n'y ai jamais retouché.

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

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.