kantien a écrit 1187 commentaires

J'ai pu le vérifier pas plus tard que dimanche dernier quand j'ai loué une voiture

Comme tu le dis par la suite, ça dépend des personnes. J'ai pu le vérifier pas plus tard que cet après-midi, où je me suis retrouvé en première dans une côte en attendant d'avoir l'espace latéral suffisant pour doubler une file de cycliste, et cela sans m'exciter derrière mon volant (ce qui n'était pas le cas de mon passager, qui pestait). ;-)

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

Pour vulgariser l'IA je dis que ça revient à "un programme dont on n'a pas l'algorithme".

Ton raisonnement (qui fonctionne par contraposition), ainsi que celui de LeBouquetin, est le suivant:

• si on a l'algorithme d'un programme, on peut anticiper son comportement dans toute situation (majeure)
• or on ne peut pas toujours anticiper le comportement d'une IA (mineure)
• donc on n'a pas l'algorithme d'une IA (conclusion)

Sauf qu'il me semble que la majeure de votre raisonnement est erronée. ;-)

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

La semaine dernière, je n'avais pas assez de temps pour développer ma pensée et revenir sur le fond de l'article du lien; aujourd'hui je le peux.

Je voudrais d'abord revenir sur un point qu'il rejette : l'encapsulation ou les types de données abstraits, résumés sous le principe "Code should not know about the internals of objects it’s working with". C'est là un principe que je ne renierai jamais, et dont les développeurs OCaml font un usage abondant : on s'en fout, la plupart du temps, de la représentation concrète d'un type, ce que l'on veut connaître c'est son interface ou API, c'est-à-dire ce que l'on peut faire avec.

J'ai toujours aimé la présentation qu'en faisait John C. Reynolds dans son article Types, abstraction and parametric polymorphism. Il présente l'idée sous la forme d'une fable où des étudiants d'université suivent des cours sur les nombres complexes. Certains étudiants ont pour professeur Descartes qui les définit comme une paire de nombres réels (partie réelle et partie imaginaire), tandis qu'une autre partie des étudiants a pour professeur Bessel qui les définit par leurs coordonnées polaires. Chacun définit ensuite les notions usuels sur les complexes. Puis au cours du semestre, les deux sections sont interchangées, et pourtant les étudiants ne rencontre aucune difficultés bien que les représentations concrètes choisies par chacun des enseignants soient distinctes. C'est cela l'essence des types de donnés abstraits.

Bon revenons à nos moutons, et à l'article qui critique ce principe pour des raisons de performances. Dans un premier temps, il ne fait pas que suivre ce principe mais applique toute la panoplie de la POO. Ensuite, au lieu de faire une hiérarchie de classes, il va définir un type somme de quatre figures et faire un switch statement pour comparer les performances. Ce qui revient à implémenter quelque chose du genre :

module Forme_simple = struct
  type t =
    | Square of float
    | Recangle of float * float
    | Triangle of float * float
    | Circle of float

  let area = function
    | Square width -> width *. width
    | Rectangle (length, witdth) -> length *. width
    | Triangle (base, height) -> 0.5 *. base *. height
    | Circle radius -> Float.pi *. radius *. radius
end

Maintenant, constatant que les formules de calculs de surfaces ont des similarité, il tente son optimisation ultime. En Ocaml cela ressemblerait à cela :

module Forme_simple_bis = struct
  type t = {
    kind : int ;
    width : float ;
    height : float ;
  }

  let square w = {kind = 0; width = w; height = w}
  let rectangle width height = {kind = 1; width; height}
  let triangle width height {kind = 2; widht; height}
  let circle radius = {kind = 3; width = radius; height = radius}

  let coeff = [|1.0 ; 1.0; 0.5; Float.pi|]

  let area {kind; width; height} = coeff.(kind) *. width *. height
end

Il y a déjà un point problématique dans son code s'il ne cache pas la représentation de son type à l'extérieur : comment garantir l'invariant qu'un carré a nécessairement une largeur égale à sa hauteur ?

Ensuite au niveau des interfaces, chacun des deux modules peuvent se voir donner exactement la même :

module type Forme_simple = sig
  type t

  (* constructeurs de formes *)
  val square : float -> t
  val rectangle : float -> float -> t
  val triangle : flaot -> float -> t
  val circle : float -> t

  (* méthodes sur les formes *)
  val area : t -> float
end

Et maintenant, il y a même mieux entre ces deux modules : algébriquement, ces deux structures sont totalement isomorphes (comme pour Descartes et Bessel dans la fable de Reynolds). Autrement dit, elles sont complétement équivalentes pour l'utilisateur et, en tant qu'implémenteur, je peux passer de l'une à l'autre sans perturber aucunement le code client, à la condition de respecter le principe Code should not know about the internals of objects it’s working with. ;-)

Enfin, si l'on revient à mon graphe de la catégorie des structures algébriques correspondantes, comme pour le type Top il n'y a pas qu'une implémentation possible pour la somme de quatre structures. Ce qu'il a constaté c'est qu'en choisissant une implémentation adaptée, on peut avoir un code plus performant. En revanche, si on ne veut pas perturber le code client de nos modules, il faut cacher les détails d'implémentation. D'ailleurs, si seule la méthode area l'intéresse, je peux lui proposer un choix encore plus drastique pour la représentation du type t, à savoir type t = float :-P Autrement dit, on calcule une bonne fois pour toute la surface à la construction (ce qui ne marche réellement que si les valeurs sont immuables ;-)

Une dernière petite remarque pour la route : ces deux modules de formes simples ne sont, par contre, pas isomorphes à la structure Top de la catégorie (celle que l'on manipule en faisant de la POO). Elles n'en sont que des sous-structures, car elles ne contiennent pas toutes les formes possibles et imaginables mais seulement quatre. Ce qui signifie que toutes le formes simples sont des formes, notion qui n'a absolument rien à voir avec l'héritage et une hiérarchie de classes (mais c'est là une toute autre histoire… ;-).

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

Je le trouve inadapté pour modéliser des concepts issus des langages fonctionnels

Ça ne sert effectivement à rien. Un jour j'ai demandé à quelqu'un de m'expliquer l'UML, au bout de dix minutes je lui ai dit d'arrêter : je n'avais rien à apprendre d'une personne qui ne sait pas structurer logiquement sa pensée de manière adéquate. En revanche j'use abondamment de diagrammes : ceux de la théorie des catégories. Bon après, j'ai une gros rejet de la POO, non du concept d'objet de la POO, mais du paradigme dans lequel tout est objet (à la Java). C'est pour moi un paradigme d'asile d'aliéné, ou l'art de faire de l'algèbre en marchant sur la tête. Je m'explique en reprenant le cas d'étude de l'article.

Qu'un carré, un rectangle ou un cercle soient des formes, il n'y a là aucun doute. Mais cette propriété n'a rien à foutre dans leur définition ! Ce qui est inévitablement le cas si on les définit comme des objets. Personnellement je les définit ainsi :

module Carré = struct
  type t = {width : float}

  let make width = {width}

  let area {width} = width *. width
end

module Rectangle = struct
  type t = {
    width : float;
    length : float;
  }

  let make width length = {widht; length}

  let area {width; length} = width *. length
end

module Cercle = struct
  type t = {radius : float}

  let make radius = {radius}

  let area {radius} = Float.pi *. radius *. radius
end

Ce qui définit chacun des types, ce sont les enregistrements et la propriété qu'ils ont d'avoir une surface se traduit par l'existence d'une fonction area sur chacun de ces types. Après le concept d'un objet, au sens de la POO, c'est le type suprême de toutes les formes, celui dans lequel on peut injecter n'importe quel forme. Ce que ne semble pas avoir compris l'auteur de l'article du lien, puisqu'il ne considère que le type somme de quatre formes possibles, alors qu'il y a aussi n'importe quel polygone, des ellipses…

Et voilà comment on définit, algébriquement, un tel type :

module type Shape = sig
  module type S = sig
    type t
    val area : t -> float
  end

  type 'a meth = (module S with type t = 'a)
  (* les valeurs de type `t` sont des formes *)
  type t

  (* toute valeur d'un type `'a` qui possède une méthode `area` est une forme *)
  val make : 'a meth -> 'a -> t

  val area : t -> float
end

Je n'ai donné que l'interface (ou API) d'un module qui définit ce genre suprême, sans préciser les détails d'implémentation ("Code should not know about the internals of objects it’s working with" ;-). Pour l'implémentation du type Shape.t je peux prendre aux choix :

• un objet : type t = < area : unit -> float >
• une clôture : type t = unit -> float
• un gadt : type t = Shape : {meth : 'a meth; self : 'a} -> t

et la liste n'est pas exhaustive.

Et c'est là qu'interviennent les diagrammes de la théorie des catégories. Une forme est caractérisée par l'existence d'une fonction area sur son type. Algébriquement cela se traduit par l'étude des structures algébriques ayant la signature Shape.S :

module type S =
  type t
  val area : t -> float
end

On peut faire un graphe orienté de toutes ces structures : chaque nœud du graphe est un module satisfaisant cette signature, et chaque arête est une fonction qui transforme un nœud en un autre (par exemple, la proposition tous les carrés sont des rectangles est représentée par une telle arrête). Mais dans ce graphe (qui, en soit, contient une infinité de nœuds), il y a un nœud particulier T (ou plutôt une famille de nœud). Ce dernier à la propriété que pour tout autre nœud N du graphe il existe une et une seule arrête qui va de N à T. Ce nœud T est le type Top de toutes ces structures algébriques, celui qui les contient toutes (les carrés, les rectangles, les cercles…). En réalité, il y a une infinité de tels nœuds Top, mais ils sont tous équivalents et ne diffèrent que par leurs détails d'implémentation (j'en ai donné 3 possibles au-dessus). La fonction centrale de cette structure c'est de faire du dynamic dispacth ou du polymorphisme ad-hoc : il applique la fonction area adéquate à la forme qu'il contient. Mais la stratégie à base d'objets et de vtable n'est qu'une solution parmi d'autre pour faire cela. On trouve par exemple, dans des langages existant :

• les modules (ou les objets) en OCaml ;
• les objets dans tout langage orienté POO ;
• les interface en Golang ;
• les type class en Haskell ;
• les template en C++ (c'est l'équivalent des modules OCaml) ;
• les traits en Rust ;
• et bien d'autres encore.

Mais pour définir une fonction sur une liste de formes, ou sur une forme quelconque, c'est-à-dire pour faire du polymorphisme ad-hoc, il n'est absolument pas nécessaire de les injecter dans le type Top (qui est le type des objets de la POO), et c'est ce que je reproche à la POO : elle réduit la catégorie à son seul objet terminal (ce type Top), ce qui est une manière plus que bancal de faire de l'algèbre. D'autant que de nombreuses catégories de structures algébriques n'ont pas d'objet terminal, à commencer par toutes celles qui ont des opérateurs binaires (addition, multiplication), où il devient alors vraiment ridicule de suivre le paradigme du tout objet.

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

Il y a bien cette citation que l'on attribue à Georges Bernanos (je ne sais si elle est apocryphe ou non) :

On ne comprend absolument rien à la civilisation moderne si l'on n'admet pas tout d'abord qu'elle est une conspiration universelle contre toute espèce de vie intérieure.

Or si l'être humain se détourne de toute vie intérieure, il ne peut combler le vide resenti que par sa vie extérieure, ce qui se traduit, inévitablement, par une augmentation sans frein de sa consommation de biens…

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

Comme toi j'hésite, surtout que cette année je vais augmenter ma surface de culture (et donc mon besoin en tuteur). Par contre, l'an dernier je me suis retrouvé avec des cultures cramées (fleur de tomates brûlées qui ne donnent pas de fruits, framboises à moitié brûlées, jamais vu ça) alors que j'avais préparé des protections anti-pluie car il y a deux ans l'excès de pluie m'avait fait perdre une partie de ma production (fraise et tomate). Résultat, je me demande si je ne devrais pas mettre en place une charpente qui s'adapte aux conditions…

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

Ç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.