kantien a écrit 1131 commentaires

Ça fait plusieurs fois que tu parles de ça, j'ai vois pas trop ce que tu veux dire par là. Tu peux développer ce que c'est cette bouteille enterrée ?

Je suppose que c'est un système DY d'arrosage en continu. Les puristes du tout naturel te vanterons la solution de l'oya, que tu peux remplacer par une bouteille en plastique (mais alors tu es dans le camp de l'enfer et de l'usage dérivé du pétrole) ou tout autre système goutte à goutte (qui rejoint le "mal" précédent).

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

C'est que le programme de Hilbert a été définitivement mis au rebut depuis presque un siècle.

Il n'a pas été mis aux rebuts, il a été réorienté : A propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court).

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

AAAAAAAAAAAAAAH…. merci. Il va falloir que j'ajoute à ma TODO d'interdire ce genre de définition (il me semble que des outils comme coq pourrait m'aider à implémenter cette fonctionnalité).

Je ne suis pas certain qu'il soit nécessaire d'interdire ce genre de définition. Dans ton langage, comme tu peux raffiner un type à l'exécution, le type object c'est juste le interface {} du Go. Tu perds toute information de typage, mais ce n'est pas en soit dangereux, juste peut utile du point de vue typage. Et si on ne peut pas raffiner le type, c'est juste un singleton (même s'il semble contenir plus de valeurs en apparence) : voir cette discussion sur le forum OCaml.

Après, d'une manière générale, comme te l'a fait remarquer Octachron, tu ne précises rien sur la hiérarchie des univers : si even et !even était dans le même univers, le type even | !even ne contiendrait pas toutes les valeurs.

Enfin, avoir une contradiction dans le système de types (vu comme une logique) n'est pas si grave si tu ne cherches pas à implémenter un assistant de preuves. Dès que tu as de la récursion générale, c'est inévitable.

let rec f x = f x;;
val f : 'a -> 'b = <fun>

(* l'équivalent de ton type `never` *)
type never = |

(* et pourtant il n'est pas vide, un calcul qui ne termine pas peut recevoir ce type *)
let _ : never = f ()

(* ou encore avec une exception *)
let _ : never = failwith "faux"

Plus d'infos sur cette présentation de la correspondance de Curry-Howard.

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

Peu importe, on est censé pouvoir additionner les deux.

Mais, on le peut ! Il est tout à fait possible d'ajouter des nombres pairs et des nombres impairs, en les considérant en tant que int. C'est juste qu'il y une annotation explicite de typage pour dire cela au type checker; mais la valeur deux de mon exemple précédent est bien à la fois de type Event.t et de type int.

Ce que tu fais, c'est du sous-typage : c'est le cœur de la logique des classes d'Aristote. J'en avais parlé lors d'une dépêche sur OCaml pour expliquer la distinction entre héritage et sous-typage, et la différence fondamentale entre le système objets d'OCaml et celui de Java (par exemple).

Il n'y pas que les objets mathématiques qui ont plusieurs types, tous les êtres sont ainsi. Par exemple, Socrate est un homme mais c'est aussi un animal, un philosophe grec… Si tu sais que tous les animaux sont mortels et que Socrate est un homme, pour pouvoir appliquer le premier principe à Socrate (et conclure qu'il est mortel), il faut justifier du fait que c'est un animal, ce que tu peux faire si tu sais que les hommes sont des animaux.

• Tous les animaux sont mortels
• Tous les hommes sont des animaux
• or Socrate est un homme
• donc Socrate est un animal
• donc Socrate est mortel

La hiérarchie entre les concepts mortel, animal, homme : c'est ça le sous-typage. En OCaml, lorsque j'écris ceci :

type t = private M.t

j'affirme au type-checker que tous les t sont des M.t ou, de manière équivalente, que t est un sous-type de M.t. Ainsi par application du principe de définition par compréhension, on obtient que tous les Event.t sont des int. Après quand je veux appliquer la fonction +, dont le type est int -> int -> int, avec parmi les paramètres la valeur deux : Event.t, il se passe deux choses. Dans un premier temps, je ne dis pas au type checker que je veux oublier la parité de deux, alors il se plaint, les deux types int et Event.t étant distincts (tous les entiers ne sont pas pairs). Par contre si je lui dis que je veux oublier sa parité et le voir comme un int en écrivant deux :> int, il valide le tout car il sait que les Event.t sont des int et que donc deux est bien aussi un int.

Cela étant, je tiens à signaler que tout ceci est réalisé statiquement (le code non annoté refuserai de compiler), ce qui n'est pas le cas de LetLang d'après tes specs. La différence étant que les cast doivent être explicites en OCaml.

Après, il y a un point non abordé dans ta spec : quid des listes de even ? Sont-elles des listes de number ? Si c'est le cas, il te faudra aborder la notion de variance (invariance, covariance et contravariance) des types paramétriques. Exemple en OCaml :

(* une fonction qui somme une liste de `int` *)
let sum l = List.fold_left (+) 0 l;;
val sum : int list -> int = <fun>

(* la somme des 3 premiers `int` *)
 sum [1; 2; 3];;
- : int = 6

(* elle somme aussi les listes de `Event.t`, le type list étant covariant *)
sum ([deux; deux] :> int list);;
- : int = 4

Je ne suis pas sûr que tu te sois posé la question, car d'après ta spec sur les fonctions, on peut lire :

NB: The class func[arguments -> return] contains every function with the same signature.

Pourtant les types des fonctions -> est contravariant sur son entrée (arguments) et covariant sur sa sortie (return). Ainsi la classe func[number -> number] devrait aussi contenir les fonctions avec cette signature func[number -> int] (si on retourne un int, on retourne aussi, a fortiori, un number).

let foo (f : int -> int) x = f x;;
val foo : (int -> int) -> int -> int = <fun>

(* je peux appliquer `foo` a une fonction de type `int -> Event.t` *)
let bar (f :  int -> Even.t) = foo (f :> int -> int);;
val bar : (int -> Even.t) -> int -> int = <fun>

Bonjour la condescendance. De une je n'ai jamais prétendu être un expert, de deux je présente un système de type inspiré de la théorie des ensembles, et non inspiré d'une quelconque théorie des types (car il y en a plusieurs).

Ce n'était pas de la condescendance, juste un peu d'agacement de ma part au ton perçu (peut-être à tort) de ton message. Et j'avais lu ta spec : tu t'inspires de l'approche de Russel et Whitehead dans leur principia mathamtica. Je voulais juste signaler que la proposition selon laquelle les objets mathématiques n'avaient pas de type été fausse (au sens IT ou non du terme, sens qui reste somme toute assez flou). Tu prends le partie de la compréhension sur celui de l'extension en ce qui concerne un concept. Un concept pouvant être envisagé de deux points de vue : celui de la compréhension (les conditions sous lesquelles un objet tombe sous un concept, ce qui en constitue sa définition) ou celui de son extension (la totalité des choses qui tombent sous ce concept, ce qui en fait une collection, un ensemble de choses). Tu prends le partie de la compréhension est en fait un fonction qui retourne un booléen, fonction qui ne sera appliquée qu'à l'exécution.

Cela étant, il y a un point qui m'intrigue dans ta spec. Tu prétends avoir rejeté l'idée d'un classe object qui contiendrait toutes les valeurs du langage, parce que cela irait à l'encontre de la hiérarchie des set. Mais qu'en est-il de cette classe que je semble pouvoir définir ?

class object (v : !even | even)

De ce que je comprends, sa fonction de compréhension vaut true pour toutes valeurs du langage, et donc l'extension de cette classe contiendrait bien toutes les valeurs.

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

Dans ton exemple, OCaml croit que l'on ne peut pas additionner des nombres pairs, ce qui est complètement faux.

Non, il demande simplement à être explicite sur le type que je donne à une valeur dans chaque contexte. Autrement dit, quand il voit la valeur deux, il demande au programmeur : la considères tu comme un entier pair ou simplement comme un entier ?

Sinon, je m'arrête là, il y a certaines notions qui semble t'échapper au sein de la théorie des types et des mathématiques en générale.

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

Devrais-je clarifier dans la LEP que quand je dis "ils n'ont pas de type" je parle de "type" au sens IT du terme?

Je ne vois toujours pas en quoi ils n'ont pas de type au sens IT du terme. Un type c'est un ensemble de valeurs (comme N, Q ou R), et la notion d'ensemble au sens "naïf", telle qu'utilisée en mathématiques, est bien plus proche de celle de type que de celle d'ensemble au sens de ZFC (personnellement, je préfère de loin les théories de types comme fondements des mathématiques à ZFC).

Après, ton système de classe revient à appliquer le principe de la définition par compréhension, ce qui génère des sous-types de ton type d'entrée. En OCaml, on pourrait formuler le principe général ainsi :

module Comprehension (M : sig type t val prop : t -> bool end) : sig
  type t = private M.t
  val make : M.t -> t
end = struct
  type t = M.t
  let make x = if M.prop x then x else failwith "make"
end

Le schéma de compréhension prend en entrée un type t ainsi qu'un propriété sur ce type, puis renvoie en sortie le sous-type (ou sous-ensemble) des éléments de t qui satisfont la propriété. Exemple avec le type even :

module Even = Comprehension (struct
  type t = int
  let prop x = x mod 2 = 0
end)

let deux = Even.make 2;;
val deux : Even.t = 2

(* ici `deux` est considéré comme de type `Event.t` et non comme `int` *)
deux + 3;;
Line 1, characters 0-4:
Error: This expression has type Even.t but an expression was expected of type
         int

(* mais on peut aussi le caster vers un `int` *)
(deux :> int) + 3;;
- : int = 5

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

Comme déjà dit par Thomas Douillard, c'est le calcul des constructions (une théorie des types) qui est à la base de Coq. Pour OCaml, le système de types qui s'en rapproche le plus c'est le système F de Jean-Yves Girard. Par contre, utiliser les modules OCaml pour éviter les paradoxes n'est pas un bon choix. Leo White a implémenté le paradoxe de Girard dans le système de modules de OCaml.

D'une manière générale, il me semble que si la logique sous-jacente d'un système de types est non contradictoire, alors le système de calcul associé n'est pas turing complet (ce qui est, par exemple, le cas de Coq); ce qui n'est pas une propriété désirée pour un langage généraliste.

Après, il y a un point que je ne comprends pas trop dans la LEP de David Delassus, lorsqu'il dit que les objets mathématiques n'ont pas de types. Pour moi les mots types et concepts mathématiques sont synonymes, donc si, les objets mathématiques ont tous un type (type qui, certes, n'est pas unique : les entiers sont des rationnels, qui sont eux-mêmes des réels, qui sont des complexes…)

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

J'ai vu plus bas Kantien partager un peu sur les aspects philosophiques liés à l'éthique ; quelques références bibliographiques seraient bienvenues pour agrémenter les soirées d'hiver qui nous attendent en cette semaine de printemps :-).

Disons que j'ai partagé certains aspects de la déontologie kantienne, déontologie qui ne fait pas l'unanimité dans les cercles philosophiques (loin de là). On peut trouver des positions conséquentialistes, utilitaristes, amoralistes… Il y a sur, la chaîne youtube de Monsieur Phi, une playliste consacrée à la philosophie morale.

Pour une comparaison entre le kantisme et le logiciel libre, il y a une conférence de Véronique Bonnet, lors d'une Ubuntu Party, intitulée « Éthique du libre : une lecture philosophique ». On peut trouver la transcription avec source vers la vidéo sur le site de l'April. En particulier, ce passage souligne la distinction que ne cesse de faire RMS entre le mouvement du logiciel libre et celui de l'Open Source :

Grand lecteur de Rousseau, Kant, et c'est là qu'il y a une dissociation décisive entre l'éthique et la morale : « Critique de la Raison Pratique » de Kant, qu'il dissocie, exprès, de la « Critique de la Raison Pure ». Dans l'Antiquité, si je veux être bon, il faut que je sois intelligent. Si je suis intelligent, je verrai bien que si je fais du mal à l'autre, eh bien, je risque d'avoir du mal aussi. Donc, si je suis intelligent, je serai bon. Pas du tout chez Kant : dissociation. Qu’est-ce que c'est que la morale ? C'est écouter la voix du devoir. Le devoir, on va retrouver cette forme-là dans les textes de Richard Stallman que je vais vous montrer, le devoir c'est une forme de « je dois ». Si je ne veux pas abîmer mon humanité, « je ne peux pas ne pas ». Si mon voisin me demande telle aide, je ne peux pas ne pas, même si ce n'est pas avantageux. Et là, vous avez donc une dissociation entre ce qui est optimal, ce qui est avantageux, et ce qui est moral. C'est une éthique qui est plus qu'une éthique. C'est une morale. […]

À mon sens, et vous allez voir que le lexique utilisé par Richard Stallman est un lexique non pas de l'éthique au sens d'Aristote, mais un lexique du devoir au sens de Rousseau et de Kant. Du devoir, « je ne peux pas ne pas ».

L'approche de RMS n'est pas ce que Kant qualifiait de pragmatique, mais catégorique : je ne peux pas ne pas donner les droits que confèrent le logiciel libre aux utilisateurs de mon code; là où un pragmatique y verra un moyen pour développer un logiciel plus sûr et stable.

Ensuite si tu veux une bibliographie sur cette approche, le plus simple est de remonter à la source : Fondements de la métaphysique de mœurs et Critique de la Raison pratique. Le première se veut un ouvrage populaire et plus simple d'accès, là où le seconde est fondamentalement un ouvrage théorique plus compliqué à assimiler, surtout si l'on n'est pas familiarisé avec la méthode kantienne.

Globalement, et pour faire très simple, son approche est analogue à celle utilisée pour typer statiquement les langages fonctionnels. Il va faire jouer la table des catégories que l'on trouve dans la Critique de la Raison pure. On la trouve ici sur wikisource. Cette table est une image en miroir de celle des jugements empruntée à la logique formelle, que l'on trouve dans le paragraphe précédent.

Lorsque l'on juge une action humaine (éthiquement-moralement ou juridiquement), on considère l'auteur de l'action comme cause d'un événement dans le monde. Ici il fait jouer la troisième catégorie de la relation (cause et effet) qui renvoie aux jugements hypothétiques de la logique formelle. C'est là que l'on voit l'analogie avec le typage dans les langages de programmations :

(* appliquer une fonction `f` à son paramètre `x` *)
let apply f x = f x;;
val apply : ('a -> 'b) -> 'a -> 'b

La fonction apply a pour type la règle du modus ponens, qui est celle que l'on utilise sur les jugements hypothétiques : si A alors B, or A donc B. On retrouve aussi son lien avec le rapport de cause à effet, lorsque l'on utilise la logique de Hoare pour analyser le comportement d'un code dans un langage impératif. C'est la règle de composition des instructions :

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

Ici la règle dit que si l'instruction S fait passer la machine de l'état P à l'état Q et que l'instruction T fait passer la machine de l'état Q ) l'état R, alors la séquence d'instructions S ; T fait passer la machine de l'état P à l'état R. Mais qui dit changement d'états, dit cause agissante…[1] Et cette règle est l'équivalent de la composition de fonctions, qui est une double application du modus ponens etc.

Bon, là c'est bien, c'est formel, tout beau tout propre. Mais si l'être humain, en agissant, est cause d'événements dans le monde, il utilise pour cela des moyens en vue de certaines fins, les fins étant les états qu'il veut voir se réaliser dans le monde. La question éthique qui se pose alors est : quelles fins sont permises, lesquelles ne le sont pas ? Quelles sont les lois qui régissent ce système de moyens et de fins ? Pour traiter cette question Kant va utiliser la logique modale, c'est-à-dire la catégorie de la modalité dans le tableau du premier lien :

• possibilité / impossibilité
• existence / non existence
• nécessité / contingence

À chaque modalité va correspondre un type d'impératifs, c'est-à-dire de règle d'action.

La première (possibilité) donne les impératifs techniques : si tu veux du pain, construis un moulin. Ici on relie une fin (je veux du pain) à un moyen (construits un moulin), parce que l'objectif est seulement possible (tout le monde ne veux pas forcément du pain).

La seconde (existence) donne les impératifs pragmatiques, ce sont des règles qui relie aussi une fin à des moyens pour y parvenir, mais cette fois la fin est considérée comme réelle (existe) pour tout le monde : la recherche du bonheur.

Viens enfin la dernière modalité : la nécessité. C'est elle qui détermine la notion du devoir, le devoir (il faut que) rendant nécessaire une action; la loi du devoir ne détermine pas tant les moyens que les fins que l'homme se doit de se proposer. Puis la nécessité d'une chose étant l'impossibilité du contraire, on retrouve le « je ne peux pas ne pas » de la conférence de Véronique Bonnet.

Enfin, pour une développement formel et détaillé de ce que je n'ai fait qu'esquisser, je renvoie aux deux ouvrages sus-cités de Kant. :-)

[1]: On pourrait, par exemple, exprimer la seconde loi de Newton avec la même syntaxe que celle du formalisme de la logique de Hoare.

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

Oups ! Il y a une double négation erronée dans ma réponse précédente. Il faut lire :

Tout d'abord, Kant n'a nullement dit (ni moi) que c'était « tout-à-fait rien » que de refuser d'obéir à l'injonction […]

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

Pas besoin d'être philosophe pour avancer un tel point, et d'ailleurs certains l'on déjà effectivement fait. ;-)

Tout d'abord, Kant n'a nullement dit (ni moi) que ce n'était pas « tout-à-fait rien » que de refuser d'obéir à l'injonction, dans une telle circonstance, afin de faire son devoir. Maintenant, faisons une petite variation sur ce dilemme, dans un contexte plus proche de toi : cette fois l'officier exige de toi que tu lui fournisses ta clef privée pour déchiffrer la correspondance que tu as avec des résistants, ce qui lui permettra de les localiser ainsi que les juifs qu'ils protègent. Même si tu ne peux affirmer que tu résisteras à toutes les tortures qu'il te fera subir, tu dois pouvoir sentir en toi que l'idée de te taire et de retenir cette information n'est pas inenvisageable; car tel est ton devoir.

Pour en revenir au dilemme précédent, que tu lui dises ou non la vérité, il y a de forte chance que ton sort soi déjà scellé. Il y a peu de chance que l'officier te croit sur paroles, qu'il vérifie lui même en fouillant les lieux avec ses hommes !

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

En y repensant je suppose qu’on peut s’en sortir en disant au patient « on vous donne un médicament OU un placebo ».

Voilà, tu as trouvé la réponse tout seul. La détention d'information n'est pas nécessairement immorale, d'autant qu'ici elle résulte clairement du contrat passé entre les expérimentateurs et les patients, qui acceptent en connaissance de cause.

La position radicale de Kant sur le mensonge a fait couler beaucoup d'encre, surtout depuis la seconde guerre mondiale et son texte polémique avec Benjamin Constant (le dernier lien de mon commentaire, sur le prétendu droit de mentir par humanité) qui peut générer ce problème éthique : si un officier nazi (disons Adolfo Ramirez, « c'est français, police française ! ») me demande si j'héberge et cache un juif chez moi, puis-je lui mentir ? Kant répondrait par la négative : tu ne dois pas mentir… mais rien ne t'oblige à lui répondre. ;-)

Sa position sur le mensonge se fonde sur sa conception contractualiste du fondement du droit. En mentant, même si l'on ne commet pas directement une injustice envers la personne à qui l'on ment, l'on commet une injustice de manière générale envers l'humanité en sapant la source de tout contrat : la confiance réciproque entre les deux parties, sans laquelle aucun contrat n'est possible.

Dans le monde du libre, il y a un contrat tacite de bonne foi entre tous les participants, contrat rompu par l'attitude des chercheurs à l'origine de l'étude. Ce qui explique la réaction de Greg Kroah-Hartman vis à vis des contributions de l'université du Minnesota. Ce thème a été également repris et bien développé par Jehan dans ce commentaire et mène inéluctablement à cette conclusion :

leur parole une fois qu'ils se sont fait prendre la main dans le sac ne vaut plus grand chose

Ainsi, une telle maxime (mentir quand ça nous arrange), si elle s'universalisait, détruirait toute confiance entre les hommes et rendrait impossible l'établissement de contrats et donc d'un état de droit stable et durable.

Dans le cas de l'étude en question, il semble, également, y avoir une entorse au principe fondamental du devoir :

Agis de façon telle que tu traites l'humanité, aussi bien dans ta personne que dans toute autre, toujours en même temps comme fin, et jamais simplement comme moyen

La tromperie dont les auteurs ont fait preuve, vis à vis de mainteneurs du noyau, semble ne considérer leur humanité que comme moyen et non comme fin : ce ne sont que de simples pions dans leur protocole; ce qui explique également la réaction vindicative de l'équipe du noyau.

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

Il y a des conditions à respecter pour que ça passe, comme

• justifier de la nécessité de la tromperie auprès du comité d’éthique;

Un comité d'éthique qui validerait une telle justification serait un comité de chien galeux!

Il peut arriver que tout ce qu’un homme regarde comme vrai ne le soit pas (car il peut se tromper) ; mais il doit être véridique dans tout ce qu’il dit (il ne doit pas tromper), que sa parole soit purement intérieure (devant Dieu), ou qu’elle soit aussi extérieure. — La transgression de ce devoir de véracité est le mensonge. Il peut donc y avoir un mensonge intérieur aussi bien qu’un mensonge extérieur ; et tous les deux peuvent être réunis, ou bien encore se contredire.

Un mensonge, interne ou externe, est de deux sortes ; suivant 1° que l’on donne comme vrai ce qu’on sait ne l’être pas, 2° que l’on donne pour certain ce qu’on sait être subjectivement incertain.

Le mensonge ( « du père des mensonges, par lequel tout mal est entré dans le monde » ) est proprement la point corrompu dans la nature humaine ; le ton de la véracité (à l’exemple de certains marchands chinois, qui mettent en lettres d’or sur leurs enseignes : « Ici on ne trompe pas » ), principalement en ce qui regarde le sursensible, est le ton ordinaire. — Le précepte : Tu ne dois pas mentir (dans l’intention même la plus pieuse), pris intérieurement pour principe dans la philosophie, comme science de la sagesse, n’aurait pas l’avantage seulement d’y établir une paix perpétuelle, mais aussi d'en assurer à jamais l'avenir.

Kant , Annonce de la prochaine conclusion d'un traité de paix perpétuelle en philosophie.

Dans l'affaire du journal les auteurs de l'étude se sont révélés doublement trompeurs et mensongers :

• une première fois, vis à vis des mainteneurs du noyau, en soumettant leurs patchs hypocrites;
• une seconde fois, vis à vis de la communauté de la recherche, en bidonnant les résultats de leur étude.

Certes la déontologie kantienne est contraignante, au point que Charles Péguy lui reprochait d'avoir les mains pures mais de ne pas avoir de mains (ce qui rejoint le point selon lequel, si l'on suit des principes éthiques, on ne peut plus rien faire), mais à aucun moment la tromperie, la duperie ou la fourberie ne peuvent être considérer comme éthiquement recevables. Quand bien même cela serait fait dans une « bonne intention » : D'un prétendu droit de mentir par humanité.

Ça me fait penser qu'il faudrait que je commande la version papier de Récoltes et Semailles de Grothendieck. :-)

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

Cette chronique est proprement scandaleuse! Si l'on peut bien accorder à Alex Vizorek, ainsi qu'à RMS, que la poutine est une insulte à la gastronomie, il reste inacceptable de s'attaquer à la blanquette de veau. :-P

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

Typiquement, pour un serveur de vote électronique, c'est le genre de techno qui serait intéressante.

D'autant qu'il existe un système de vote électronique à l'état de l'art en OCaml : Belenios. Il a été présenté sur le blog de vulgarisation de la Société Informatique de France, (a voté) Euh non : a cliqué.

C'est ce que j'ai lu de plus intéressant sur un OS en 2021.

Si le sujet t'intéresse, il y a une interview d'Anil Madhavapeddy, le créateur de MirageOS, sur le thème What is an operating system ? Où l'on y apprend entre autre que l'hyperviseur Xen est né d'un pari dans un pub de Cambridge (la bière anglaise donne des idées) et que la première version de MirageOS servait à tester les couches bas niveau de Xen.

À titre personnel, un des passages qui m'a bien plu sur le choix du langage :

And OCaml, in my mind, is a generational language. One of the properties I want from systems I build is that they last the test of time. It’s so frustrating that a system I built in the early 2000s, if you put it on the internet today, would be hacked in seconds. It just would not survive for any length of time. So how do we even begin the discipline of building systems that can last for, forget a decade, just even a year without having some kind of security holes or some kind of terrible, terrible flaw?

Now, there is one argument saying that you should build living systems that are perpetually refreshed but also we should have the hope of building eternal systems that have beautiful mathematical properties and still perform useful, utilitarian functions in the world.

Passage immédiatement suivi par cette question de Yaron Minsky :

There’s one big downside I feel like I see in all of this which you haven’t talked about yet which is it requires you to write all of your code in OCaml. And I really like OCaml, you really like OCaml, it’s in some sense not a downside, but if you’re trying to build software that’s broadly useful and usable and can build a big ecosystem around it, restricting down to one particular programming language can be awkward.

Just to say the obvious, I would find it somewhat awkward if there’s some operating system I wanted to use and I had to use whatever their favorite language was and I couldn’t write in my favorite language. How do you think about this trade off?

lire la suite :-)

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

Pareil pour le coup des expansions de path, ça fait quelques décennies qu’on sait que c’est un gros problème. On évite de faire ça en root, en général.

Je dirais plutôt que suivre les liens symboliques, lors d'une suppression, irait à l'encontre de la sémantique qu'on leur donne; ils représentent des références sur les données contenues dans le répertoire cible. Si un ramasse-miette, lorsqu'il rencontre une référence, ne se contentait pas de simplement la supprimer mais supprimait aussi, au passage, les données référencées, ça poserait de sérieux problèmes en soi (quand bien même je suis le propriétaire légitime des données en question).

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

Mais ta description du problème prête à malentendu.

Effectivement, mais c'est parce qu'il y avait une incompréhension de ma part. Je pensais que le code Rust suivait les liens symboliques (ce qui eut été étrange et discutable, mais pourquoi pas) et donc qu'il faisait un test pour éviter l'élévation de privilège, test contourner ensuite par l'attaquant via la race condition. Mais l'attaque est en faite plus subtile que cela, comme décrit par Gof.

Un programme root ou assimilé qui accepte de détruire des données sur la requête de n’importe qui, c’est un accident qui attend d’arriver comme ils disent outre quebin.

Là si je parlais de mandat accepté et donc de requête utilisateur, c'est parce que je prenais le point de vue de l'attaquant qui en jouant sur les liens symboliques construits (de son point de vue) une requête pour le programme cible, qui lui ne voit pas du tout cela comme une requête mais comme une action légitime de suppression de son point de vue. Que l'attaquant transforme un répertoire en lien symbolique, ou modifie la destination du lien, de son point de vue cela ne change rien : il construit une requête de suppression pour augmenter ses privilèges.

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

du point de vue du système, il a bien les droits de le faire

Encore heureux, sinon ce ne serait pas un bug dans la bibliothèque Rust mais dans le noyau.

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

L'appel système de suppression est fait en mode privilégié ?

Oui, c'est un problème d'escalation des privilèges, raison pour laquelle je parlais des services de l'État (qui eux peuvent, sous condition, exproprier et détruire la maison de n'importe qui).

Le problème existe lorsque ce code Rust est utilisé par un utilitaire système en mode privilégié, alors je peux me servir de lui pour effacer un répertoire sur lequel je n'ai aucun droit. Dans l'exemple qu'ils donnent, ce pourrait être un utilitaire qui fait le ménage dans /tmp, alors en créant un lien symbolique dans /tmp je peux effacer tout ce que je veux avec les même droits que l'utilitaire.

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

On parle bien de supprimer des fichier auquel l'utilisateur qui les supprime a bien les droits de suppression.

Ce n'est pas ce que j'ai compris, et c'est tout l'intérêt de la race condition. Je mets un lien symbolique vers un répertoire sur lequel j'ai des droits, le code Rust vérifie que c'est bien le cas et accepte d'agir en mon nom (je le mandate), puis avant qu'il suive le lien pour en effacer le contenu, je change la destination vers un répertoire sur lequel je n'ai aucun droit et là paf le chien. La race condition est là : entre le check et l'effacement effectif.

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

La gestion des permissions, quand à elle, reste correcte d'un point de vue système

Même là c'est douteux. Si les services de l'État viennent détruire ta maison, sous ce très pernicieux prétexte, que j'en ai mis l'ordre de mission sur leur bureau, je doute que tu considères que la gestion des permissions reste correcte d'un point de vue système. ;-)

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

Ce langage est trop matheux à mon goût.

C'est une question de goût : personnellement, c'est pour cela que je l'aime. Un ordinateur, ça sert à calculer et tout ce qui s'éloigne, de près ou de loin, de la pratique mathématique en la matière, finit irrémédiablement à la poubelle chez moi. De plus, les mathématiciens, outre leur quête de rigueur, ont un penchant naturel pour une recherche d'esthétisme dans leur notation et la structure de leur discours : esthétisme que je ne retrouve pas dans les autres langages.

Les mathématiques ont un triple but. Elles doivent fournir un instrument pour l’étude de la nature.

Mais ce n’est pas tout : elles ont un but philosophique et, j’ose le dire, un but esthétique. Elles doivent aider le philosophe à approfondir les notions de nombre, d’espace, de temps.

Et surtout leurs adeptes y trouvent des jouissances analogues à celles que donnent la peinture et la musique. Ils admirent la délicate harmonie des nombres et des formes ; ils s’émerveillent quand une découverte nouvelle leur ouvre une perspective inattendue ; et la joie qu’ils éprouvent ainsi n’a-t-elle pas le caractère esthétique, bien que les sens n’y prennent aucune part ? Peu de privilégiés sont appelés à la goûter pleinement, cela est vrai, mais n’est-ce pas ce qui arrive pour les arts les plus nobles ?

Henri Poincaré, la valeur de la science

Tu dois avoir des problèmes de souvenir sur ce que te disait ton prof.

Ton explication par exemple de :
val compare : t -> (t -> int)

Je me rappelle de mon prof qui disait qu'on pouvait le lire aussi:
val compare : (t -> t) -> int

Donc ça prend une fonction de t vers t et ça renvoie un int (qui de mon point de vue se rapproche davantage du "je prends 2 arguments et je renvoie un entier vrai/faux".

Je ne vois pas comment tu peux lire la seconde signature comme "je prends 2 arguments", alors qu'elle n'en prend qu'un qui est une fonction. De plus, on ne peut pas lire la première comme la seconde, mais celle-là est équivalente à une fonction avec cette signature :

val compare : t * t -> int

qui se lit déjà mieux comme "je prends 2 arguments…". Mais quand je dis qu'elles sont équivalentes, je ne veux pas dire que ce sont les mêmes, mais que je peux passer de l'une à l'autre et qu'elles calculeront la même chose. Le passage de l'une à l'autre se nomme curryfication mais ce n'est absolument pas propre à OCaml, comme l'illustre l'article de wikipédia. Ce passage de l'un à l'autre, ou cette équivalence, est identique à cette identité algébrique sur l'exponentielle et le produit :

(A ^ B) ^ C = A ^ (B * C)

L'exponentielle c'est le type des fonctions (la flèche -> lue de droite à gauche) et le produit c'est le produit cartésien sur les types (pour créer des paires).

La version à la Curry permet de définir simplement des clôtures ou des applications partielles, comme dans cet exemple :

List.map (compare 2) [1; 2; 3; 4; 5]

D'ailleurs, au sens propre du terme, une fonction n'a toujours qu'un seul argument. Dans la version non curryfiée, il se trouve que cet unique argument est une paire (d'où la lecture "je prends 2 arguments…"), ce qu'il n'est pas dans la version à la Curry.

En ce qui concerne, l'intérêt des fonctions qui retournent des fonctions (t -> (t -> int)) et des clôtures, tu pourras lire la discussion que l'on a eu récemment sur les génériques dans Go. Ici @wilk donne un lien vers un article qui, pour présenter la notion de clôture en Go, définit justement une fonction qui retourne une fonction.

Je ne pourrai jamais m'intéresser à un projet codé en (O)Caml, aussi intéressant puisse-t-il être.

Je n'aime pas l'ananas mais je crois, qu'ici, tout le monde s'en fout, et je ne vois pas bien l'intérêt d'exprimer la chose publiquement. Dans le cas présent, je doute que les auteurs du projet puissent être, pour leur part, intéresser pas les contributions que tu pourrais apporter.

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

Bon, quand on regarde en détail, je préfère

int compare(a: T, b : T);

(les fonctions façon LISP… pour compare et add dans cet exemple) à

val compare : t -> t -> int

C'est une question de point de vue, et je trouve la syntaxe OCaml bien plus cohérente quand on la regarde dans l'ensemble du langage.

Une expression de la forme val e : t se lit « e est une valeur de type t », et je ne vois pas pourquoi il faudrait changer de forme, sous prétexte que la valeur compare est ici une fonction. Le : de OCaml c'est comme le epsilon () des mathématiciens, il signifie l'appartenance à un ensemble. Ici, c'est l'ensemble des fonctions des t vers les fonctions des t dans les int (ça se lit t -> (t -> int)), c'est une fonction qui renvoie une fonction. De même, la fonction successeur sur les entiers a pour type int -> int, c'est une fonction des int vers les int.

En résumé, on a donc un nom pour la valeur, suivi du : (le epsilon des matheux, ou le est du français comme dans « Socrate est un homme ») puis enfin une expression qui appartient au langage des types.

Cette dernière expression, on pourrait la réutiliser telle quelle dans le langage des types, pour définir par exemple un type paramétrique, comme ici :

type 'a comparator = 'a -> 'a -> int

Ici comparator est une fonction des types dans les types (un type paramétrique) et 'a est le nom de son paramètre. On peut alors réécrire la signature du début ainsi:

(* la fonction `comparator` appliquée au type `t` *)
val compare : t comparator (* t -> t -> int *)

Il y a en fait 4 langages dans OCaml :

• le langage des valeurs et expressions
• le langage des types des expressions
• le langage des modules
• le langage des types de modules ou signatures

Les deux derniers, dont tu préfères la syntaxe, ont « globalement » les même principe syntaxiques que les deux premiers qui semblent te désarçonner. Pourquoi ?

Pour le foncteur Make, on aurait pu écrire sa signature ainsi :

module Make : functor (S : ORDERED) -> sig ... end

ce qui est la même syntaxe que pour compare, à part le mot clef functor (personnellement, je le trouve inutile et j'aurais préféré qu'il soit absent, je trouve qu'il alourdit sans raison l'écriture et la lecture).

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

Je ne vois pas de fermeture dans l'exemple que tu donnes par contre ?

Les fonctions Abs sont des fermetures, une interface c'est un dictionnaire de fermetures. Prenons le code d'usage de l'interface :

func main() {
    var a Abser
    f := MyFloat(-math.Sqrt2)
    v := Vertex{3, 4}

    a = f  // a MyFloat implements Abser
    a = &v // a *Vertex implements Abser

    // In the following line, v is a Vertex (not *Vertex)
    // and does NOT implement Abser.
    a = v

    fmt.Println(a.Abs())
}

la variable a est un dictionnaire de fermeture et a.Abs est une fermeture (la variable capturée étant soit un Myfloat, soit un *Vertex). Il en est de même pour n'importe quelle interface. C'est pareil en POO : un objet c'est un dictionnaire de fermetures qui partagent le même environnement (les variables d'instance). C'est un usage classique des fermetures pour faire du polymoprhisme ad-hoc, qui est celui que tu décris, avec de l'encapsulation. Cela permet d'utiliser, comme expliqué dans l'article que tu cites sur medium, le même algorithme sur différentes structures de données qui partagent un comportement commun (décrit par l'interface).

Voyons voir ce qu'est une fermeture (je l'écris en OCaml, c'est plus simple pour moi, surtout pour la suite).

let foo i j = 2 * i + j

ici la fonction foo est dite close car toutes les variables qui apparaissent dans son code sont des paramètres formels de celle-ci. En revanche ce n'est plus le cas celle-ci:

let i = 2
let bar j = 2 * i + j

ici la variable i fait partie de l'environnement de bar (on dit que i apparaît libre dans bar, là où il est lié dans foo), cette dernière est une application partielle de foo: let bar = foo 2. La fermeture consiste à transformer bar en une paire constituée de la fonction close foo et du paramètre i = 2 : une fonction non close est transformée en une fonction close, on la clôture ;-)

Reprenons maintenant l'interface Abser de l'exemple en go:

type Abser interface {
    Abs() float64
}

En OCaml, on écrirait cela ainsi :

type abser = { abs : unit -> float }

mais ce type sera habité par des fermetures, c'est à dire des paires dont la fonction close aura cette forme :

type 'a abser_close = { abs : 'a -> float }

et la clôture aura cette forme :

type 'a abser_closure = 'a abser_close * 'a

autrement dit une fonction sans variable libre sur une type 'a, ainsi qu'une valeur de ce même type 'a correspondant à celle qui est capturée et encapsulée dans la clôture. Maintenant le type de départ abser est équivalent à la réunion (ou somme) sur tous les types possibles des fermetures précédentes :

type abser = Abser : 'a abser_closure -> abser

Géométriquement, on peut représenter cela par un cône:

La base circulaire représente tous les types possibles du langage et le sommet est justement le type abser. Ce cône peut être vu comme un graphe orienté étiqueté, où chaque arrête va de la base vers le sommet avec comme étiquette la fonction qui calcule la valeur absolue pour le type en question. Il illustre comment on transforme un Myfloat ou un *Vertex en un Abser. Maintenant, quand on veut utiliser un Abser, il faut retourner l'orientation du graphe : on ne va plus de la base vers le sommet, mais du sommet vers la base. Alors une valeur de type Abser ne peut être utilisée quand observant la valeur qu'elle encapsule, en redescendant le long de l'arrête correspondant et en appliquant la fonction en étiquette. Ce mécanisme d'utilisation d'un Abser est ce que les programmeurs appellent le dynamic dispatch, qui est au cœur de la POO et du polymorphisme ad-hoc.

La généricité, en revanche, permet d'appliquer le même algorithme sur un même structure de données qui est un conteneur, comme le sont les tableaux (on parle plutôt volontiers, dans ce cas, de polymorphisme structurel). Ici, vous vous en sortez avec des fermetures (comme pour la fonction de tri), parce qu'un tableau peut être vu comme un dictionnaire clef-valeur où les clefs sont des int. Ainsi, au lieu d'avoir une fonction avec un type polymorphe, qui prend une fonction de comparaison sur le type contenu dans le tableau ('a -> 'a > bool), vous pouvez vous contentez d'un type monomoprhe int -> int -> bool en encapsulant le tableau et en accédant aux valeurs par leur index. Mais cela réduit la généricité au tableaux, qui sont built-in, et cela ne permet pas de créer ses propres type génériques.

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

Je ne sais pas.

Moi non plus. Ce qui me fait douter du fait que wilk comprenne bien ce qu'est le système de interfaces, ainsi que le manque que vient combler le système des génériques. L'idée derrière ce système étant de pouvoir retrouver, dans le système de types, le type de la variable capturée dans l'environnement des fermetures que constitue l'interface. Alors qu'avant il pouvait seulement le retrouver par un switch sur type dans le code (d'où le nombre important de code qui prennent un interface {} en entrée). Il pouvait réfléchir dans le code, mais non dans le système de types, la structure de l'environnement de leurs fermetures.

Si on prend l'exemple de a tour of go:

type MyFloat float64

func (f MyFloat) Abs() float64 {
    if f < 0 {
        return float64(-f)
    }
    return float64(f)
}

type Vertex struct {
    X, Y float64
}

func (v *Vertex) Abs() float64 {
    return math.Sqrt(v.X*v.X + v.Y*v.Y)
}

On voit bien, sur leur déclaration, que les deux méthodes Abs sont des fermetures : la première capture un MyFloat et la seconde un *Vertex. Les génériques permettent juste de donner un nom de variable au type de la valeur capturée pour l'utiliser dans la signature des fonctions.

soit n'ont pas besoin de ça

Ça fait un peu « dis moi ce dont tu as besoin, je te dirais comment t'en passer ».

soit tu te crée que des méthodes et pas des fonctions. Tu modifie les paramètres que l'on te donne plutôt que de retourner quelque chose.

Même le tri en place du tableau, je doute que ce soit possible (génériquement) en golang avec seulement des interfaces (pour la bonne raison qu'une fonction d'ordre est un opérateur binaire, ce qui n'est pas gérer par les interfaces de base).

Après, qu'il existe des contournements, en l'absence de généricité, pour résoudre les problèmes que l'on a, je n'en doute pas. Là où je suis plus sceptique, c'est qu'ils auront plutôt tendance à compliquer le code et non le simplifier.

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

Le code n'a plus de lien avec le type de l'objet capturé avec la fermeture, mais avec le comportement de la fermeture elle même.

J'aurais du préciser : sans perdre le lien entre le type d'entrée et le type de sortie. ;-)

Sinon ce que tu décris c'est tout simplement le fonctionnement des interfaces jusqu'alors : une interface c'est juste un dictionnaire de fermetures. D'ailleurs pourquoi passer par des fermetures à sa sauce quand le langage fournit nativement un tel mécanisme ?

Un cas d'exemple simple et générique impossible à rendre, au niveau des types, avec les interfaces (ou fermetures) : le tri d'un tableau. Quand on a un tableau sur un type ordonné (que le type soit ordonné cela s'exprime par le fait qu'il satisfait une certaine interface), alors on peut trier (par ordre croissant ou décroissant) ce tableau : le type de sortie dépend du type de l'entrée, en sortie on a un tableau sur le même type de données qu'en entrée.

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