kantien a écrit 1248 commentaires

Sauf que changer un type de base qui est utilisé dans les binding C

Je ne vois pas où ils ont changé un type de base, ils ont juste changé la signature d'une fonction. Avant on avait :

int div(int i, int j)

maintenant on a :

float div(int i, int j)

C'est juste le type de sortie d'une fonction qui a changé, non la représentation en mémoire d'un type de base. C'est un léger changement d'interface et de sémantique pour une fonction, avec une autre fonction existante (//) ayant le même comportement que l'ancienne, pas de quoi fouetter un chat ni jouer à l'équilibriste en haut d'un immeuble de 42 étages par vent de force 5. ;-)

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

il a fallu changer tout python

Non, juste redéfinir une fonction sur un type de base. Je n'appelle pas cela changer tout le langage. ;-)

Python 2.7.13 (default, Nov 24 2017, 17:33:09) 
[GCC 6.3.0 20170516] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from __future__ import division
>>> 2/3
0.6666666666666666
>>> 2//3
0

Pour la question de l'absence de typage statique, c'est loin d'être le seul défaut de python.

Pour rester sur la question de la rigueur mathématique, de toute façon, pour moi, dès qu'on sort de la programmation fonctionnelle avec typage statique, on n'est déjà plus très rigoureux (je tolère à la rigueur les effets de bords et le code impure, c'est-à-dire les valeurs mutables, mais au-delà de ça, on est trop loin de la conception mathématique du calcul).

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

Je reviens à ce que je dis : s'il-te-plait, donne moi un avantage du float par rapport au Decimal mis à part la perfo.

Dès que l'on quitte les opérations algébriques de base (addition, multiplication, soustraction) et qu'on en vient aux fonctions transcendantes¹ (sinus, cosinus, logarithme, exponentielle…, voir le commentaire de Michaël). Si tu reprends l'article de Guido sur les raisons du changements pour la division sur les int :

(This recently happened to me in a program that draws an analog clock – the positions of the hands were calculated incorrectly due to truncation, but the error was barely detectable except at certain times of day.)

Pour dessiner une horloge analogique, il faut faire de la trigonométrie et donc utilise les float. ;-)

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

C'est même pire que ce que tu crois, il faudrait changer également l'inteprétation des littéraux.

type(2.3)
<class 'float'>

Je t'explique pas les problèmes de retro-compatibilité s'il fallait les interpréter par des décimaux :

type(2.3)
<class 'decimal.Decimal'>

il faudrait rajouter des float(...) partout dans le code existant :

type(float(2.3))
<class 'float'>

Ils n'ont pas déjà assez de problèmes avec le passage python 2.7 vers python 3 ?

Si tu veux des décimaux et gérer manuellement tes arrondis (et des problèmes d'arrondis, tu en auras), il y a un module pour cela : decimal. Si tu veux du calcul exact sur des fractions (sans problèmes d'arrondis avec les opérations algébriques), tu as un module pour cela : fractions. Sinon par défaut, comme dans tous les langages, tu te retrouves avec des nombres à virgule flottante ce qui n'est pas sans raison.

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

Merci de lire le 3e point de la page de la doc de Python. C'est exactement de ça dont je parle, c'est exactement la solution au problème exposé dans ce journal.

Eh bien ce que tu souhaites exactement (par défaut) est profondément ridicule. Quitte à choisir une représentation pour avoir de l'exactitude dans les calculs et perdre du temps (inutile dans la quasi totalité des applications), autant choisir celles des fractions : avec les décimaux tu n'as même pas la structure de corps (c'est pas « stable » par division comme type de données).

>>> from decimal import Decimal
>>> i,j = Decimal(3), Decimal(5)
>>> i * (j / i)
Decimal('5.000000000000000000000000001')
>>> (i * j) / i
Decimal('5')

>>> from fractions import Fraction
>>> i,j = Fraction(3), Fraction(5)
>>> i * (j / i)
Fraction(5, 1)
>>> (i * j) / i
Fraction(5, 1)

Maintenant que Python switche tout seul de l'int à l'IEEE quand il le juge bon, va-t-il un jour switcher de int à Decimal à IEEE quand il le juge bon ?

Et je t'ai répondu que ce n'est pas ce qu'il fait ! Il a juste changer la sémantique de l'opérateur / et son type de sortie. Avant / calculait le quotient euclidien et était de type int * int -> int, maintenant il calcule le résultat de la division en flottant et est de type int * int -> float. C'est juste un changement de sémantique (l'opérateur // étant là pour la division euclidienne) et non une adaptation au besoin de précision. Si vraiment, ils avaient voulu cela (ou s'ils le voulaient) il faudrait choisir le type Fraction en sortie et non le type Decimal.

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

C'est sûr que c'est pas très lisible pour un CM2. :-P

L'écriture est lié au système de typage statique OCaml qui n'a pas de mécanisme à la type classes de Haskell. Du coup 2 est toujours interpréter comme étant de type int et ~$ est juste une notation infixe pour la fonction of_int.

L'idée était surtout de montrer qu'il n'y avait aucune difficulté à faire du calcul formel sur les rationnels, avec pour seul limite la capacité mémoire de la machine (python le fait aussi) : c'est juste coûteux en mémoire et plus long en calcul, mais inutile dans la plupart des applications (d'où le recours aux flottants par défaut dans tous les langages).

>>> from fractions import Fraction
>>> # attention à bien utiliser des strings
... Fraction('2') - Fraction('1.8') - Fraction('0.2')
Fraction(0, 1)
>>> # avec les floats sa posera aussi problème
... Fraction(2) - Fraction(1.8) - Fraction(0.2)
Fraction(-1, 18014398509481984)
>>> Fraction('3') * Fraction('5/3')
Fraction(5, 1)

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

Je me dis aussi que vu que Python le fait déjà dans un autre cas

C'est pas tout à fait cela, il a changé la sémantique d'un de ces opérateurs sur les int, à savoir l'opérateur /, qui avant calculait le quotient euclidien et qui maintenant calcule la division dans le type float (ce qui ne change pas les problèmes d'arrondis et l'impossibilité d'avoir une représentation finie en base 2 pour certaines fractions).

Si tu veux calculer formellement sur des fractions en python, il faut utiliser le module fractions.

>>> from fractions import Fraction
>>> # attention à bien utiliser des strings
... Fraction('2') - Fraction('1.8') - Fraction('0.2')
Fraction(0, 1)
>>> Fraction('3') * Fraction('5/3')
Fraction(5, 1)
>>> # avec les floats ça posera aussi problème
... Fraction(2) - Fraction(1.8) - Fraction(0.2)
Fraction(-1, 18014398509481984)

Pour avoir un jour un tel comportement par défaut, j'en doute : les besoins en calcul formel sur ce type de nombres sont trop rares (application de niche) pour en faire le comportement par défaut.

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

Avec Zarith et la précision arbitraire sur les entiers et les rationnels, on résout le problème du journal :

#require "zarith"
#install_printer Q.pp_print
#install_printer Z.pp_print

let i = Q.(~$5 / ~$3);;
val i : Q.t = 5/3

Q.(~$3 * i);;
- : Q.t = 5

Q.(of_int 2 - of_string "18/10" - of_string "2/10");;
- : Q.t = 0

mais aussi celui d'un de tes anciens journaux ;-)

Z.(shift_right one 64);;
- : Z.t = 0

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

Oui, je l'ai trouvé après le pretty-printer. Je l'ai mis dans cet autre commentaire et celui-ci. C'est plus joli avec. ;-)

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

les décimaux ne forment qu'un anneau et pas un corps

mais les rationnels, eux, forment un corps :

let i = Q.of_int 3 in
let j = Q.of_int 5 in
Q.(i * (j / i));;
- : Q.t = 5

:-)

et pour ceux qui aiment les grandes puissances :-P

pow 2017 2017;;
- : Z.t =
3906579755433725744549801881596227303161113974786331742808014316352404207866781011779432579441775839856
9303675091317686485769854660061633900821022073493790844484206374523765685047888592941732567957896337356
8227616903361285861720928485319957896879451656212960334524148908182859288925011902051241977461866923828
5805141216845194646359692773930173890452130301484108603704907663185918027996588306289045733101837983728
0327741427585781943934907066383115733602932268165774793029250948453140731624523723322353528718052018269
2120301190715379956212549955472924854051368917564413054345164976023589951663964251322964845660608570604
8796166013211776531223294858858770618287202956153159070909025445244612929266907435405734058205954066196
6257944413954048938877964772886958563547919584266955161383320262256139624507335975998767755685814334472
7668109856905808726786650150176346749276701349195925308447304906625583450532575618820393030470662264833
6558516764477800855702247701966133115392119659229044822591905333270631043927666037528178491629195538568
4646233989829228655115524936994639184750912047564895374720764672140695409095592363173332472459576462404
5478715399572715756795527704408680018385825873357580378471551915354156980027304848137549295408442862472
0693653228246725934999526408544103045213286398414699798897380577563918878645812125863807732821991332107
8692725905849174024449511921146294190262906996085368959603576478405323143384080388379319554908856556731
5908088452296187414871507326380105914169781913896257814769011618619675396354441317274069735446648347083
9685322479279715610244075962909647201924726552325770866912670386908832937068991644217985561454518613500
7701134281137791471069061199195503527692941530730806868244125447916029477919365350907160212555600592600
7272962151491655468415250273052830341020248623946192353295309806703225240777982731701762090578986703739
2654445594383017249413223433802591420751864046339582968716946613883883630089289092850166742420098475615
2317270292569678698976098602918745091738269938053862716103474442695166725670001543967580405510009441047
9024451590607819278757744377853151071774880174452988351732344899456989727677340502177914005216463498939
1224975421083168091648327063033553252608930068052730798133922253562033497135729065886319850700135166684
4733145986594861443630941669140652635251193447008192851553865779612842872522984948643907872238326400270
9446351625648515268700769721875710891517353990646067011044373315111199657801536917591352152223077856196
7585937746338830459587033526143098022187621420524532754885931847288027594032004390130183176362334815608
9447394688706409250220073258561438553336541717486859130299187109664700107919273459900361576563360385933
3122333043348929219564612801024584337753852145099150440931873218035637881859414477740279483748996993268
2275112162153565809151704179070457180504206906398450192005390333618194565994404545750817781718292706125
0315795328152260735534962635462010401164107240551217025457278458627050670150520970059759320354286441883
9562193815774326236977529972966261410337323664706113705568867451193992124787596100597886820452817195495
5020000700127981453761067545668056756361891835461795143007732741778254730545511658948801939623478920322
8770082758023203322668981651809246482681180422142387309386716816318069955940334056256140580819497179850
3289109355115029124983991018380698424651876194056194282127149997079562496102454369536500984933908739935
9218078735267669384753478767335747571773444969818858147423712760105039603697963834693464702773990816319
6468633747558552065688014667143037574127092846695111905537504841894849764673682096326975021012366606664
0911512953157476533586025093593927262144788949918692089397761431261871877904288178513169823048344238328
2260926947373572812701186712470174863056734569600082502717603716470089407418211450488493170968284198629
6783490416745451108403140493810716002978244023457593747581792541662690908599087691849588468048336655885
3396587675219737345520051486671981990599704130000418965813007224733672096313749475119407724014818508929
5435174820956072871376082451787665388114475605020203864631818413786212782294741026763089059841440923141
7930945943586389649372607933085049704786949757073506895518158455729471986353589128929298803482871893326
4617496210897466235050589604540196335236324754935438515933094258601062968745635884513724512140377812087
9963194898376112183936544916070097706168459234442106763663835372336483086417102786616287430017146620033
9061917369717038449238804553048471167262994455769562518460603987773119867917673314811942882902518952778
4452428862612449080278884098946247489646956505581906115889044658676526114959262438720723867498045450888
6534081710593801600793606848908583050665498686794547787119719610041793592240855296660979007332421390030
6864863782743260903304031347797201921526690054472717597175870696793550292948276452471679162724097409195
9226574012956618385918903583572362462995750127092270563921014720062585125823141782751812643109647530407
8716782263312492623267010550372864203265543683594017627021586771839427413268536947121551554157057847039
0705555753425386733887289438493039753930209202288508301197091965403738469234797311845916566136505553919
5347218311488110187672218257397856026847785288284864740137044134948049741708836860375429551872331945923
3479018544074018576809852216096689981623517895747450086026777001537987227211508713435225975549765258124
8620911163696461283347058836782766473033926630818043689367183277879852758810482761319983832255793901827
2344962449422866729130494318349786441889312965949010199609058366877816005182554357929793751308237195750
8857847106213666743133998010213985877939816967416366993032326406723766280172424741817792379452453933339
1257817923012542366733267840996910829815897656293583783006983681960984012935500660931269066599266830614
9298048454144277912938192170665670364309688124177002766249617224562497248029025108484112804667962930792
7246554758514993911161605836359758869768035926923821402027569506890143101867597868188376534215289800688
4850534058152513832422421443657177753062012002238067078120526881695766025581633086349571371749861205684
2009287332050038500758131655474444270464394270810368067423747143094562220685933183169518338219129062478
9016636657171699043027493231137226070566921703173674515116874346577116337134958859551451311536998094430
8436603930597247181404703316361315782728069013669316656084882670461314916661537994490564226822718247595
6096597627288520629228771111807430370106408669790774313609604966005455290197434687532220849212300973638
4079162882379305241098491933927011736912353861798242466005141298986845754182687703787699360707018541512
82858987245060220859376040188961430411125280662489310010991839503913438177

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

Mon prof de math justement, t'aurais mis 0, tu n'as pas indiqué la précision.

Il écrit des nombres décimaux, ce sont des valeurs tout a fait acceptables dont on n'a pas besoin d'indiquer la précision (sinon on indique un intervalle).

#install_printer Q.pp_print;;

Q.(of_ints 2 3 * of_ints 3 4);; (* 2/3 * 3/4 =  1/2 *)
- : Q.t = 1/2

Q.(of_string "2" - of_string "18/10" - of_string "2/10");; (* 2 - 1.8 - 0.2 = 0 *)
- : Q.t = 0

Q.(of_int 2 - of_float 1.8 - of_float 0.2);; (* avec les float ça marche pas *)
- : Q.t = -1/18014398509481984

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

Par exemple, en bc, 3*(5/3) ne donne pas 5.

Mauvais système de calcul formel ⇒ changer système de calcul formel :

Q.(print @@ of_int 1 * of_string "5/3");;
5/3- : unit = ()

Q.(print @@ of_int 3 * of_string "5/3");;
5- : unit = ()

let i = Q.(of_int 3 * of_string "5/3");;
val i : Q.t = {Q.num = <abstr>; den = <abstr>}

Z.(to_int (Q.num i), to_int (Q.den i));;
- : int * int = (5, 1)

Zarith :-)

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

D'autant que si on n'a pas déjà installé faketime, c'est plus long. Je ne sais pas comment fonctionne tous les systèmes, mais sur le mien ça ne fout pas le bordel. Si je n'enchaîne pas les deux commandes via le ;, mais l'une après l'autre, l'heure est déjà revenue à la normale.

$ date +%T -s "00:30:00"
00:30:00
$ man; date +%T
Quelle page de manuel voulez-vous ?
19:30:29

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

Exact, il a du le modifier entre temps. Dans la version que j'ai c'est bien à minuit et demi. Voir le commit qui le retire.

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

Pour ma part, j'ai appris le système des bases en primaire. De mémoire, on avait un certain nombre de croix, de batons ou de points que l'on devait regrouper en ensemble de n éléments, puis on devait regrouper les groupes en surgroupes de n groupes, et ainsi de suite.

Itou. :-) De mémoire c'était surtout en CM1 et CM2 que l'on pratiquait ce genre d'analyse.

On avait également vu les règles de division par 3 ou 9 pour des nombres en base 10 avec compréhension de leur principe. Pour savoir si 54 est divisible par 3 (sans chercher dans ses tables ou effectuer la divison), il suffit de faire 5 + 4 = 9 et de constater que 9 est divisible par 3 donc 54 aussi. Le principe est simple quand on a compris le fonctionnement des bases : 54 c'est 5 paquets de dix et un paquet de 4. Or quand on divise un paquet de dix en trois personnes, chacun en a trois et il nous en reste un sur les bras. Donc avec cinq paquets, il nous en reste cinq sur les bras, plus les quatre unités cela fait neuf unités, que l'on peut alors répartir en trois par personnes.

Je me servais de ce genre de principe dans la cours quand on faisait du « plouf, plouf, amstramgram » pour choisir les membres de son équipe de foot : je savais par qui commencer pour avoir celui que je voulais, sans rien laisser au hasard. Les joies de l'arithmétique modulaire. :-)

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

Pour continuer sur le même exemple, combien de bacheliers sont bien à l'aise avec les changements de base (de numération) ? C'est pourtant ça le recul indispensable à enseigner les techniques opératoires élémentaires au CP.

Il y a du y avoir des changements, avec les époques, sur ce qui était enseigné tant aux élèves qu'aux enseignants. Si je prends mon expérience personnelle : dans les années 80, à la sortie de mon primaire on nous avait appris le changement de base (essentiellement la conversion base 10 vers base 5, mais des fois aussi base 2 ou 3). Lorsque j'étais étudiant, je donnais des cours particuliers pour financer mes études : certains de mes élèves de terminale (en terminale S) galéraient pour la conversion base 10 vers base 5. Et pour la formation de mes institutrices : la plupart avaient fait l'école normale sans être bachelières. ;-)

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

D'après l'article d'Europe1, le communiqué de la Fédération des Aveugles de France contiendrait ce passage : « Pour nous personnes aveugles, cette soi-disant langue inclusive est proprement indéchiffrable par nos lecteurs d'écrans ». Je m'inscris totalement en faux contre cet argument en vertu du principe, déjà invoqué, suivant : « c'est pas compatible avec les lecteurs d'écran pour malvoyants » est un argument faux, émis par quelqu'un qui n'a jamais testé ces lecteurs. En effet, il va de soi que les aveugles n'ont jamais testé les lecteurs d'écran et sont les moins à même d'en parler. :-P

P.S : ceci étant dit, je n'ai pas réussi à trouver le communiqué en ligne sur leur site, bien que plusieurs journaux en parlent.

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

Un générateur d'onde sinusoïdale, dans le domaine audio, c'est proche d'un "Hello World!". ;-)
Après on peut jouer sur la fréquence ("Hello @hpiedcoq!") ou même la forme du signal ("@hpiedcoq, les sinusoïdes c'est la base du traitement du signal ;-)"). :-)

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

Ça se discute, tout dépend à qui se réfère l'adjectif épithète. Ces trois phrases me semblent correctes, mais n'expriment pas la même chose :

• une des plus brillante scientifiques du siècle dernier est, sans hésitation, Marie Curie
• une des plus brillants scientifiques du siècle dernier est, sans hésitation, Marie Curie
• une des plus brillantes scientifiques du siècle dernier est, sans hésitation, Marie Curie

dans la première, seule Marie Curie est qualifiée de brillante.

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

Si la phrase 'par la méthode de condorcet' fait partie de la discussion, on voit bien dans l'original anglais que c'est mentionné

Comme tu le soulignes, la référence à la méthode de scrutin à la Condorcet est mentionnée sur l'original chez Debian (fait qui est notoirement connu pour quiconque connaît un minimum le fonctionnement de l'organisation Debian).

Dans un commentaire de mon journal, je précise que la mention à cette méthode était un clin d'œil à certains journaux de l'époque (on était en pleine campagne présidentielle, et certains journaux parlaient de méthodes de votes alternatives). L'introduction même du journal est une allusion au contexte historique et aux débats de l'époque sur le site.

Dans un commentaire d'un de ces journaux, en date du 15 mai, je parle de Condorcet et Borda et de mon intérêt pour ces méthodes qui remonte au moins à l'élection de 2002 et le second tour Chirac - Le Pen.

Dans la dépêche, je développe cette partie sur les modes de scrutins avec lien vers un dossier sur le site Images des Maths du CNRS.

Je pense qu'il se peut fort bien que les deux soient de bonne foi

J'ai du mal à comprendre où l'on peut voir, de bonne foi, dans mon article (et sa version promue en dépêche) une contrefaçon du sien.

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

Pas du tout, à des souvenirs traumatisants du professeur qui ponctuait ses corrections par des références à l'évidence même sans réel explication.

Au temps pour moi, avec le sujet de la dépêche, j'ai du me sentir visé : dans l'autre journal j'avais fait un appel à l'évidence et tu m'avais répondu que même si cela paraissait évident, il fallait démontrer que la solution proposée apportait quelque chose.

Pour ce qui est de l'appel à l'évidence, dans l'enseignement, c'est toujours délicat : l'évidence est très subjective (ce qui est évident pour l'un, ne l'est pas forcément pour l'autre) et dans une correction, ce n'est pas le meilleur endroit pour y faire appel.

Ceci étant, même Coq a une notion d'évidence avec la tactique trivial :

Remark a : forall n, 0 + n = n + 0.
Proof.
trivial.
Qed.

mais en réalité, il trouve cela trivial car il applique directement un théorème qui est dans sa base de données (et qui énonce la même chose). En revanche, la preuve du théorème initial n'est pas triviale pour la machine, il faut la faire à la main par récurrence; là où avec un interlocuteur humain, un mathématicien serait tenté d'écrire : évident par récurrence sur n (en précisant toutefois le mode de démonstration à utiliser).

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

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.

Oui j'étais au courant, j'ai eu des échanges téléphoniques et par mails avec Benoît. En revanche je ne suis pas dans la procédure, il semble que je ne suis pas juridiquement impliqué dans l'affaire (bien que d'un point de vue moral, je le sois indubitablement). J'ai envoyé des éléments de défense pour nier la qualification de contrefaçon tant de l'article que de la dépêche.

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

Ou mieux : demander à kantien de le réécrire.

Ce qu'ils ont fait lors de sa promotion en dépêche.

Si le journal était purement factuel et reprenait la forme et le contenu de mes deux sources¹ :

• https://www.debian.org/vote/2017/vote_001.en.html ;
• https://bits.debian.org/2017/04/results-dpl-elections-2017.html.

La dépêche (dont je suis également l'auteur) est autrement plus fouillée et détaillée, tandis que le journal s'apparente plus à une dépêche AFP.

Ce qui repose l'éternel débat sur le choix terminologique de linuxfr entre dépêche et journal. :-P

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

Je ne sais pas quelle formation tu as eu, mais la question de la qualité dans le développement logiciel c'est loin d'être généralisé même aujourd'hui, que ce soit en entreprise ou dans les formations.

C'était une formation en logique mathématique et sur les fondements de l'informatique. Personnellement, à l'époque, la partie fondements de l'informatique ne m'intéressait pas spécialement. Je voulais surtout approfondir mes connaissances en logique et voir ce qu'avaient donné les attaques contre la philosophie kantienne des mathématiques (j'ai lu la Critique de la Raison Pure à la fin de ma spé, et je suis kantien depuis cette époque). Pour ceux intéressés par l'informatique, d'après la brochure sur les débouchés, il semblerait qu'ils finissent par faire une thèse et de la recherche (dans les organismes publiques ou en R&D chez des industriels genre EDF).

J'ai bien conscience qu'une telle formation est à part par rapport aux formations courantes des ingénieurs informaticiens.

Déjà, je dirais que pour être rigoureux intellectuellement, il faut démontrer que la solution proposée apporte quelque chose. Même si cela paraît évident. Car comme je l'ai dit, ce n'est pas parce que ton travail provient de la recherche universitaire que cela est forcément bénéfique. On ne va pas lister le nombre de prédictions théoriques de la recherche fondamentale (dont sur les noyaux de système d'exploitation) qui n'ont jamais su percer dans l'industrie faute d'adéquation en réalité.

Démontrer comment, par l'exemple ? Mais, de mon point de vue, un fait ne prouve pas grand chose : je m'intéresse surtout aux méthodes et à leur limite. Je suis un obsédé de la certitude : qu'est-ce que la certitude ? de quoi peut-on être certain ? quelles méthodes peuvent espérer atteindre à la certitude, lesquelles ne le peuvent pas ? font partie des questions qui m'obsèdent. Et de ce point de vue, l'induction et la méthode expérimentale reviennent à cela :

l'expérience ne donne jamais à ses jugements une universalité vraie et rigoureuse, mais seulement supposée ou comparative, si bien que cette universalité doit proprement signifier : Pour autant que nous l'ayons perçu jusqu'ici, il ne se trouve pas d'exception à telle ou telle règle.

Kant, introduction de la Critique de la Raison Pure.

ou pour citer Einstein résumant la philosophie sceptique de Hume : « l'empirique, dans la connaissance, n'est jamais certain (Hume) ». Il ne fut néanmoins pas convaincu par la réponse kantienne aux objections de Hume : « Kant propose alors une pensée. Sous la forme présentée elle est indéfendable mais elle marque un progrès nette pour résoudre le dilemme de Hume ». Pour ma part, je la trouve on ne plus défendable, et la méthode qu'il employa est analogue à celle utilisée par tous les systèmes de types des langages de programmations. Pour pousser le distinguo à l'extrême : je n'ai aucune certitude que le soleil se couchera se soir, mais je n'ai aucun doute quant à ce qu'exprime le théorème de Pythagore.

Pour revenir aux outils d'analyses et de sécurisation de code, il ne s'agit pas nécessairement de spécifier dans les moindres détails chaque bout de code et d'apporter la preuve du respect de la spécification, mais il est peut être envisageable d'ajouter certaines annotations en commentaires (à la manière de frama-c) pour avoir un système de type à l'expressivité plus riche que celui du C. Le système de type de C, de fait, exprime des spécifications sur le code mais, comme c'est peu ou prou la logique propositionnelle du premier ordre, on ne peut pas y exprimer grand chose : ce que fait le code et comment l'utiliser est beaucoup trop sous-spécifié avec un tel système de type.

Prenons un exemple. Je ne connaissais Coccinelle que de nom, je suis allé voir un peu leur site, et sur la page consacrée aux évolutions collatérales ils donnent deux exemple : ajout d'un argument à une fonction et changement dans le protocole d'initialisation des pilotes. Il semblerait que les pilotes aient mis un certain temps à s'adapter correctement à ce changement d'interface dans le cœur du noyau. Ces changements il faut bien les documenter quelque part ? Pourquoi pas dans une langue proche par sa syntaxe et son vocabulaire de l'anglais, mais à la grammaire plus régulière, et l'écrire en commentaire du code modifié ? On pourrait alors avoir une logiciel d'aide à l'audit qui détecterait automatiquement les mauvais usages des nouveaux codes.

Entre un audit totalement manuel et un audit partiellement automatisé, dans le monde de l'informatique ça doit pouvoir convaincre (pourquoi faire à la main ce qu'une machine peut faire pour moi ?). Je ne suis membre d'aucune des deux communautés (celle du noyau et celle de la recherche), mais je sais que la seconde est en état de fournir ce genre d'outil à la première. Néanmoins, pour cela, il faudrait une coopération et une synergie entre elles qui ne semblent pas exister aux dires de gasche. Je ne peux que trouver cela dommage.

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