Re: l'assignation ne va jamais venir

C'est vrai que les justifications du type mais c'est évident ! ressemble fort à un prof de maths qui ne souhaite pas expliquer la solution en détails. :-)

Hé ! ce ne serait pas une allusion déguisée à certains de nos échanges récents sur un autre journal. :-P

Je ne suis pas prof de maths, et ce à quoi je faisais allusion c'est ce genre de chose :

/*@
requires \valid_read(a + (0..n-1));
requires \valid_read(b + (0..n-1));
assigns \nothing;
behavior all_equal:
 assumes \forall integer i; 0 <= i < n ==> a[i] == b[i];
 ensures \result;
behavior some_not_equal:
 assumes \exists integer i; 0 <= i < n && a[i] != b[i];
 ensures !\result;
complete behaviors;
disjoint behaviors;
*/
bool equal(const value_type* a, size_type n, const value_type* b);

extrait du livre ACSL by example (où ACSL signifie ANSI/ISO C Specification Langage). Il me semble évident que le système de type défini par ACSL est plus riche et permet de mieux exprimer la spécification de la fonction que ne le fait celui du langage C, qui dit juste que la fonction renvoie un booléen (ce que fait également la fonction qui renvoie constamment true). Qu'il existe un logiciel qui vérifie automatiquement que le code satisfait cette spécification, c'est un fait, il suffit de le tester.

Mais restons dans le sujet de la dépêche : la contrefaçon. Kant (oui, encore lui) a écrit un article sur le sujet en 1785 : De l'illégitimité de la contrefaçon des livres, article à la lecture fort intéressante et d'actualité, comme l'illustre la première note qui rappelle furieusement le problème des DRM :

Si un éditeur essayait de soumettre quiconque voudrait acheter son édition à la condition de se voir poursuivi pour soustraction d’un bien étranger à lui confié, dans le cas où, soit par son propre fait, soit par l’effet de sa négligence, l’exemplaire qu’il aurait acheté aurait été livré à l’impression, on n’y consentirait pas volontiers, car on ne voudrait pas s’exposer à toutes les importunités des perquisitions et des justifications. L’édition resterait donc sur les bras de l’éditeur.

Le texte est aussi une illustration de la rigueur, tant logique que juridique, avec laquelle Kant pouvait faire usage de la syllogistique.

Il reprendra, en 1797, le même thème dans sa Doctrine du droit dans un annexe aux droits des contrats sous le titre Qu'est-ce qu'un livre ?

La cause de ce qu'il y a d'apparamenent légitime dans une illégitimité qui saute pourtant aussi vivement aux yeux, du premier coup d'œil, que celle de la contrefaçon des livres, tient à ceci : le livre,d'une part, est un produit matériel de l'art (opus mechanicum) qui peut être imité (par celui qui se trouve en posséder légitimement un exemplaire, et par conséquent il y a là un droit réel; mais, d'un autre côté, le livre est aussi un pur et simple discours de l'éditeur au public, que le possesseur n'a pas le droit de reproduire publiquement (praestatio operae) sans avoir pour cela été mandaté par l'auteur — ce qui définit un droit personnel, et dans ces conditions l'erreur consiste en ce que l'on confond les deux droits.

Kant, Doctrine du Droit.

Sans entrée dans le détails, le droit des contrats relève du droit personnel (droit de contraindre une personne à une certaine prestation) et le genre d'annotations de code comme illustré ci-dessus est ce que l'on appelle la programmation par contrat. Elles expriment quelque chose du type : si les entrées vérifient certaines conditions alors la sortie en vérifiera d'autres. Il se trouve que Kant a donné pour fondements aux droits personnels la forme logique des jugements hypothétiques (si A alors B), tandis que les droits réels (droit de propriété sur une chose) ont pour fondements la forme logique des jugements catégoriques (A est B), ce qui correspond à la relation de sous-typage (comme je l'ai expliqué ailleurs).

Autrement dit, les débats sur la légitimité ou l'illégitimité de la contrefaçon tourne autour de la confusions entre la relation de sous-typage et le type d'une fonction.

En espérant que ce cas d'école illustrera ce que je voulais exprimer lorsque j'ai écrit un jour : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. ;-)

Pour le détail, il faut se référer au contenu des théories concernées. :-)

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