On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.
et donc les argumentations diagonales à la Cantor ne s'appliquent pas.
À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.
Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :
Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique)
Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F…), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.
Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.
à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je répondais à quelqu'un qui disait que les tests unitaires étaient limités par rapport au raisonnement mathématique. Sauf qu'en vrai on a introduit les test unitaires parce que le raisonnement mathématique était limité (pas impossible, mais insuffisant).
Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).
Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.
Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.
Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard… perdre du temps est sans doute leur objectif premier.
Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.
Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.
(* le premier je le fais en deux temps *)letrecfx=fx;;valf:'a->'b=<fun>(*puis la je l'applique sur unit mais on peut prendre n'importe quoi *)f();;(* jolie boucle infinie, on fait Ctrl-C *)(* le second je le code en OCaml *)(* la fonction identité c'est la tautologie A ⇒ A *)letidx=x;;valid:'a->'a(* maintenant j'en fait une version restreinte avec un type fantôme *)typefaux;;letf(p:faux)=p;;valf:faux->faux
Le problème avec f serait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de type faux alors que celui-ci est sans constructeur donc vide (ou inhabité).
Le passage de Rice à "les mathématiques ne sont pas possibles" est à mon avis un bel exemple d'extension abusive d'un résultat scientifique, comme on en lit souvent sur le théorème de Gödel ou sur la physique quantique. Je ne suis pas trop sûr de vers où part cette discussion.
Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).
Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Cela est fort possible, je ne connais pas les problématiques d'optimisation liées à l'évaluation paresseuse (dans un terme (fun x -> une expression avec x) t, on substitue les occurrences de x par le terme t puis on beta-réduit et on mémoïse pour ne pas avoir à recalculer t si on en a nouveau besoin; là où OCaml commence par évaluer ou beta-réduire le terme t avant de substituer puis évaluer le tout). Mais effectivement comme un terme, dans les stratégies paresseuses, se trouve « pris » dans un thunk, cela doit rejoindre sur certains points la différence entre calcul flottant boxé et unboxé en OCaml.
Je voulais juste signaler que l'implémentation des optimisations décrites dans la dépêche doit prendre en compte la possibilité d'existence d'effets de bord permis par le langage (comme pour pouvoir propager un terme par exemple), ce qui n'est pas le cas en Haskell.
Il s'agit, il me semble, de deux problématiques d'optimisations orthogonales. D'ailleurs si on fait de l'évaluation paresseuse en OCaml (avec lazy et Lazy.force) cela doit être peu ou pas du tout optimisé, non ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse à la dépêche OCaml 4.03.
Évalué à 1.
Dernière modification le 03 mai 2016 à 19:20.
Tu avais noté mon commentaire dans un coin à l'époque (qui n'est pas si lointaine d'ailleurs…) ou tu l'as recherché aujourd'hui ? :)
Je l'avais noté dans un coin de ma tête, et je l'ai recherché aujourd'hui. Je m'en suis souvenu car à l'époque (pas si lointaine effectivement, sinon ce serait sans doute sorti de ma mémoire), j'avais fait des recherche pour savoir ce qu'est la SOA et comprendre ta problématique. J'en avais retenu l'idée qu'un WSDL est une façon de décrire la spécification d'un service, et qu'engendrer du code OCaml à partir de cela c'est similaire à de la transpilation.
Quand j'ai regardé encore plus récemment la vidéo de Gérard Berry (vraiment intéressante à regarder, je le conseille si on a le temps : 1h40 avec les questions du public), ça m'a rappelé mes réflexions sur le sujet et comme le sujet du TD est un cas pratique d'un principe plus général qui s'applique aussi à cette situation, je me suis dit : autant le partager.
Pour les problématiques de pédagogie et de didactique, je n'ai pas de réponse non plus, encore moins s'il s'agit d'informatique. La seule discipline que j'ai enseignée, il y a bien des années maintenant, dans le supérieur était les mathématiques; et ce que j'ai retenu de cette expérience est : je suis un bien piètre enseignant. :-/
Cela étant, en ce qui concerne la programmation et l'apprentissage d'un langage, l'approche par la pratique et on aborde les problèmes au fur et à mesure qu'on les rencontre de facto est sans doute moins rébarbatif et plus compréhensible.
Sinon, pourquoi faire de l'inférence de type sur papier ? ça doit être ennuyeux ? Je n'ai rien contre la théorie de la démonstration et la déduction naturelle, mais quand on apprend un langage de programmation ce ne doit pas être la première chose que l'on recherche, non ? Et il y a vraiment des gens qui présentent les tests unitaires en mettant un bouquin de Popper dans les mains de leurs étudiants ?
Sur Popper (j'ai du mal avec son principe de falsification) et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens… :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse à la dépêche OCaml 4.03.
Évalué à 1.
Dernière modification le 03 mai 2016 à 16:00.
Pourtant ce type de TD, et les notions abordées et mises en pratique à travers lui, pourrait t'être fort utile pour développer des bibliothèques qui ne font pas partie de l'écosystème OCaml et dont tu sembles avoir besoin. Je cite cet extrait de ton message de l'époque :
Mais il reste encore des points sur lesquels ces langages sont à la traîne (pas du point de vue technique, mais dans les librairie existantes). Surtout dans le domaine du web. Des choses auxquelles je pense :
La gestion des web service : à ma connaissance, OCaml n'a pas de bindings pour créer un client WS à partir d'un WSDL et garantir que les données transmises sont conformes.
La gestion du XML : j'aimerai beaucoup pouvoir garantir qu'une transformation XSL appliquée sur un schéma XSD d'entré me produit un XML conforme à un XSD de sortie. (quel que soit le xml bien sûr)
Tu ajoutais que c'est techniquement possible, ce qui est tout à fait vrai et met en pratique les mêmes idées que dans ton transpilateur : voir la conférence de Gerard Berry l'importance des langages en informatique. En particulier, pour le problème concerné, à partir de la 50ème minute1 : « il faut arrêter de penser qu'il y a une syntaxe concrète à un langage, la syntaxe abstraite doit commander : c'est elle la véritable syntaxe du langage. La syntaxe concrète ne doit être qu'une façon commode pour nous de représenter la syntaxe abstraite », suivi de « XML : une syntaxe concrète pour la syntaxe abstraite » et je rajouterai avec information de typage. ;-)
Cette vision du XML constitue aussi, dans un autre domaine, une des originalités de XMPP : les principes à la base des mécanismes de typage dans les langages comme OCaml s'étendent aux protocoles réseau (j'y avais fait allusion dans la discussion qui avait suivi ton message que j'ai cité), et on le retrouve dans la nature même des message échangés dans le fonctionnement d'XMPP. Je n'insinue pas que les concepteurs de XMPP avait cette idée en tête, je n'en sais absolument rien, ils ont peut être simplement fait comme M. Jourdain qui faisait bien de la prose sans le savoir…
cela étant, la totalité de la conférence mérite d'être regardée : elle est très instructive. :-) ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse à la dépêche OCaml 4.03.
Évalué à 3.
Dernière modification le 03 mai 2016 à 12:00.
Je confirme, sa présentation de la problématique était claire avec des exemples illustrant parfaitement les optimisations réalisables, une synthèse avec traduction étant amplement suffisante.
La présentation de Flambda sur le blog de jane street est aussi une lecture intéressante, en particulier sur les exemples choisis : différentes approches au niveau des paradigmes de programmation qui, néanmoins, génèrent le même code.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je suis content de voir que le sujet de l'optimisation des performances est bien pris en compte, j'avais plusieurs fois entendu dire qu'il n'y avait que peu d'optimisation (qu'elles restaient haut niveau).
Les optimisations restent toujours haut niveau. Leur principe est connu depuis longtemps, elles n'étaient juste pas implémentées (ou pas de manière aussi poussée). In fine, ce sont somme toute des opérations élémentaires sur des termes du lambda-calcul : les réduction du l'ambda-calcul (sous-leur noms en apparences ésotériques, la beta-réduction, par exemple, est juste la transformation qui correspond à l'exécution du code, et c'est elle qui est utilisée en partie dans le processus d'inlining).
Contrairement à un langage fonctionnel pur comme Haskell, l'implémentation en OCaml demande plus de soin à cause de la manipulation de valeurs mutables. Mais ils restent encore des optimisations à effectuer, comme les opérations sur les flottants.
Certains auraient même souhaité l'intégration d'« assembleur » inline pour, par example, optimiser le calcul vectoriel en utilisant les jeux d'instuctions SSE.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
L'intêret de mon commentaire ? Où est le jugement ?
zurvan me dit que 150€ pour un téléphone ce n'est pas la mer à boire. Je lui objecte que ce tarif (pour quelqu'un qui a pas connu le monde antérieur, autrement qu'en tant qu'enfant) a de quoi suscité des interrogations. Et donc je réitère mon propos : où as-tu vu que 150€ pour un téléphone est une dépense standard ? Et tu appelles cela un jugement ?
Mon propos n'est pas de culpabiliser ceux qui peuvent se payer ce type d'outils (je le peux aussi, là n'est pas la question, et je ne me flagelle pas tous les soirs avant de me coucher), ni de dire que libre est synonyme de gratuit, mais de pointer du doigt que 150€ pour un téléphone, cela en fait rire plus d'un (rire surtout jaune).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Où est le mépris dans mon propos ? J'aimerais bien qu'on me le signale afin que je puisses adapter mon discours. Peut être n'avons nous pas la même notion du mépris.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je ne suis pas Dieu, je n'ai pas les compétences (telle l'omniscience) pour faire ce genre de chose. ;-)
Sinon, je ne suis pas toujours d'accord en tout point avec l'auteur de l'article qui, bien qu'il s'en défend, fait de la réimportation du fondement de la doctrine libérale (elle trouve ses origines sur notre continent, mais elle a été en partie oubliée, puis elle fût en partie cultivée outre atlantique mais son retour est complètement défiguré).
L'auteur est aussi dans le comité de direction de L'institut Coppet qui est une réédition d'un institut ayant existé à la fin du 18ème et au début du 19ème, dont un des membres originels s'est trouvé pris dans une polémique avec Kant : pour moi, Kant en ressort vainqueur (polémique sur les notions de droits et de devoirs).
en moins de dix minutes.
On ne lit pas à la même vitesse.
C'est fort possible, mais je pense que c'est surtout parce que les questions abordées me sont familières donc ma « lecture » se limite surtout à du déchiffrement de signes alphabétiques.
Pour la promesse que je t'ai faite de réagir sur « vendre du libre », plus la discussion/dispute sur le sujet libre /open source, je crains de ne pouvoir la tenir : entendre par là que mes réponses ne seront pas faites aujourd'hui (je doute d'avoir le temps libre pour cela).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Mais on peut trouver des téléphones potables entre 150 et 300 €, par exemple à l'époque le nexus 4 (300 €) que j'ai gardé plus de 3 ans, le moto g (170 €) que j'ai conseillé à de nombreuses personnes etc.
Il n'y a rien qui te choque ?
Je n'ai jamais vraiment eu de téléphone avant d'Android apparaisse.
La réponse à ma question doit se trouver là. ;-)
P.S. : ce n'est pas une question d'android ou non, mais de smartphone = téléphone.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
C'est pas que je suis opposé à tes propos, sur le fil de la musique libre je te suivais un message sur deux; mais là, je ne comprends même pas ce que tu veux exprimer.
Pourtant je t'ai déjà vu intervenir sur des sujets qui abordés des erreurs de syntaxes et de grammaires, et sur le coup, ta syntaxe m'est incompréhensible : que veux-tu dire ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
N'importe quoi, les paquets synchronisés depuis Debian sont au minimum recompilés. Et Ubuntu a son propre noyau, ses propres versions d'un bon nombre de paquets, héberge toute son infrastructure, a une équipe dédiée au suivi de la sécurité…
Ils sont tellement recompilé que sur ma Debian, sans trop jouer l'enfer karmique est du passé (là, si on suit les principes, Debian torche Archelinux les doigts dans le nez), avec les back-ports cela passe pour les novices. Pour le reste, j'attends une meilleure solution.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Un petit supplément sur le libéralisme : celui qui croit que notre gouvernement actuel cède aux sirènes du libéralisme, que le politique de rigueur est libéral, celui-ci est, pour moi, comme un homme qui croit qu'un hacker est un cracker parce que c'est ce qu'on lui répète à longueur de journée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
libéral regroupe beaucoup de tendances dont des gens qui ont le libéral sélectif (il y a des "libéraux" contre le mariage homo par exemple, ce qui n'est pas logique, ils se disent libéraux mais sont plutôt économiquement libéraux et socialement non libéraux). Perso je vois mal comment on peut être non libéral quand on est libriste, car c'est laisser les gens libres de faire des choses dans les deux cas (même en copyleft, si si).
Je dirai plutôt social-libéral si il faut catégoriser (la liberté des gens oui, mais avec un minimum de protection sociale type revenu universel et hôpitaux pour tous, car sans protection sociale pour donner une sécurité sur le vital point de liberté réelle)
C'est pour cela que j'avais mis un lien ;-) J'ai regardé les tiens, tu aurais pu regarder le mien; d'autant que les tiens sont des vidéos qui représentent 1h30 de temps, là où moi c'était un texte qui se lit en moins de dix minutes. Et tu aurais vu (ou plutôt lu) que les opposants aux mariages gay n'étaient pas ranger dans la catégorie « libéral » par les libéraux eux-mêmes, mais dans la catégorie « conservateur ».
Tu ne peux pas demander à autrui un acte (consulter les liens qu'il te propose et qui font partie de son discours, ce qui n'est rien d'autre qu'une liaison vers une bibliothèque externe) que tu ne fais pas toi même lorsqu'il te répond. ;-)
P.S. : je t'accorde, tout de même, que le terme « libéral » étant tellement galvaudé en France que je suis habitué à ce type de réponse. Le libéralisme n'est pas une doctrine économique, mais une doctrine juridique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Tu ne serais pas un libéral pur jus par hasard (ce n'est pas un grief sous ma plume) ?
J'ai 2-3 questions à te poser sur la stratégie employée pour faire passer FFV1 auprès des archives autrichiennes, mais ça attendra demain (il y aura peut être du troll sur free / open source, demain c'est trolldi et tu as sacrément tendu la perche, mais je ferai en sorte de faire la part des choses1 ;-)
à moins que tu considères qu'il vaille mieux que je scinde mes propos en deux messages afin de ne pas brouiller inutilement la discussion (ce qui, à bien y réfléchir, est sans doute la meilleure solution). ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Mais en pratique, les entreprises préfèrent généralement demander une petit fonctionnalité qu'ils payeront plus ou moins cher, ou de la maintenance/support, ça passe mieux au niveau hiérarchique. Bref, l'administratif n'est pas un problème si en face le développeur le veut (asso, micro-entreprise… Ou vraie entreprise).
D'ailleurs, n'est-ce pas justement ce qu'il explique dans la première vidéo au sujet du codec FFV1 (vers la 35ème minute) quand l'Archive Nationale Autrichienne a voulu faire des archives sans perte ?
Bien que je n'ai pas tout compris au passage : il compare au choix de la bibliothèque du Congrès (qui a fait un choix propriétaire), puis il dit que les décisionnaires ont décidé d'allouer le budget à une solution propriétaire, pour finir par dire qu'il ont pris ffmpeg et payer pour des fonctionnalités, ce qui leur a coûté bien moins cher, et qu'avec l'argent qu'il restait ils ont pu payer un développeur pour améliorer leur infrastructure. Ils ont réussi à faire changer d'avis les décisionnaires ?
P.S : qui est donc ce lossless Lee ? :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Pour Java, oui, il y en a : je viens à l'instant de mettre à jour open-jdk sur ma Jessie.
De toute façon, un système sans faille de sécurité est un système dans lequel on n'a pas encore trouvé la faille. Rien que depuis le début de l'année chez Debian.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Non mais je pense que j'aurai le même inconvénient , c'est à dire principalement le défilement à l'intérieur d'un fenêtre qui doit se faire avec l'ascenseur alors qu'on a envie de "glisser" comme sur une tablette.
Pourquoi ? Sur mon portable, je fais le défilement à deux doigts (verticalement ou horizontalement) avec mon touchpad : pourquoi le comportement serait différent sur un écran tactile ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Oui, mais ça c'est parce que le système des droits d'auteur actuel est complètement pourri que c'est la croix et la bannière pour faire des œuvres dérivées.
Je vais faire mon kantien, pour une fois, est exposé son point de vue sur la contrefaçon (position prise en 1784 par rapport au problème de la contrefaçon des livres), mais dont les problématiques sont bien encore d'actualité.
Que puis-je faire avec l'exemplaire d'une œuvre qui est mien ? La propriété de cette exemplaire me donne-t-elle le droit d'en faire une copie et de la livrer au public, ou est-ce attenter à mon droit sur cet exemplaire que de me l'interdire ? Problème actuel : les DRM (cf. note de bas de page graissée).
Ceux qui croient que la faculté d'éditer un livre découle de la propriété d'un exemplaire de ce livre (que cet exemplaire soit un manuscrit de l'auteur ou une copie imprimée par un précédent éditeur), et qui pensent en même temps que cette faculté peut être limitée par la réserve de certains droits, soit de l'auteur, soit de l'éditeur institué par lui, en ce sens que la contrefaçon en peut être interdite, — ceux-là n'arriveront jamais ainsi au but. Car la propriété qu'un auteur a de ses pensées (si l'on accorde qu'il y a une propriété de ce genre fondée sur des droits extérieurs) lui reste toujours acquise, indépendamment de l'impression ; et, si les acquéreurs d'un livre ne peuvent donner un consentement exprès à une semblable restriction de leur propriété [1], à combien plus forte raison un consentement qui n'est que présumé est-il insuffisant à les lier !
Je crois être fondé à considérer une édition non comme le trafic que l'on ferait d'une marchandise en son propre nom, mais comme une affaire gérée au nom d'un autre, c'est-à-dire de l'auteur, et je pense pouvoir prouver aisément et clairement de cette manière l'illégitimité de la contrefaçon. Mon argument est contenu dans un raisonnement qui prouve le droit de l'éditeur, et que suit un second raisonnement destiné à réfuter la prétention du contrefacteur.
[1] : Un éditeur oserait-il imposer à quiconque achète un ouvrage de sa maison d'édition comme condition de risquer une inculpation pour usage abusif d'un bien étranger qui lui a été confié, au cas où il se servirait intentionnellement ou même par imprudence de l'exemplaire qu'il vent à des fins de contrefaçon ? Il est douteux que quiconque donnerait un tel consentement, parce qu'on s'exposerait ainsi à tous les désagréments que vous réservent enquêtes et responsabilité. L'éditeur serait constamment sur son dos.
On retrouve, quinze ans plus tard, dans sa Doctrine du droit les mêmes considérations.
La cause de ce qu’il y a d’apparemment 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 posséder légitimement un exemplaire), et par conséquent il y à la 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 d’un exemplaire n’a pas le droit de reproduire publiquement (praestatio opera, droit de disposer d’un travail) 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.
Ce passage se trouve en appendice au chapitre sur le droit des contrats à la question Qu'est-ce qu'un livre ? Le tort du contrefacteur consiste à parler au nom de l'auteur alors qu'il n'a pas été mandaté pour cela : il fait usage d'un droit personnel qu'il n'a tout bonnement pas légitimement acquis (il lui faudrait l'accord explicite de l'auteur pour cela), droit personnel qui ne peut se déduire en toute bonne foi du droit réel qu'il possède sur son propre exemplaire.
C'est sur cette ambiguïté entre droit réel et droit personnel que joue les grands éditeurs pour coller des menottes numériques à tout va. Les DRM porte atteinte au droit réel de l'acquéreur sur son exemplaire qui, de facto, n'a plus la pleine propriété sur son bien : cela mérite plus le terme de contrat de location que celui de contrat de vente. Ce genre de pratique devrait tout bonnement être illégale.
J'avais lu un jour, mais je n'ai pas retrouvé (bon, je n'ai pas cherché très longtemps), un rapport de la quadrature du net pour le Parlement Européen sur le droit d'auteur, et ce qui m'avait surpris c'est qu'il se concentrait uniquement sur le droit réel tout en faisant l'impasse sur le droit personnel : c'est comme s'ils étaient tombés dans le piège des majors en acceptant les termes du débat. Je fût d'autant plus étonné que le rapport était écrit pas des juristes de la quadrature.
Peut-on copier un œuvre artistique, effectuer une traduction ou faire une œuvre dérivée sans le consentement de l'auteur ?
Les œuvres d’art, comme choses, peuvent être au contraire, sur les exemplaires qu’on en a légitimement acquis, copiées ou moulées, et ces copies publiquement vendues, sans que l’on ait besoin pour cela du consentement de l’auteur de l’original ou de ceux dont il s’est servi pour exécuter ses idées. Un dessin que quelqu’un a esquissé ou qu’il a fait graver par un autre, ou encore qu’il a fait exécuter en pierre, en métal ou en plâtre, peut être reproduit ou moulé par celui qui a acheté cette production, et vendu publiquement sous cette forme, comme tout ce que l’on peut faire en son propre nom d’une chose qui vous appartient, sans avoir besoin du consentement d’un autre. La dactyliothèque de Lippert peut être copiée et mise en vente par quiconque en est possesseur et s’y entend, sans que l’inventeur puisse se plaindre d’une atteinte portée à ses affaires. Car c’est une œuvre (opus, non opera alterius) que tous ceux qui en sont possesseurs peuvent, sans même indiquer le nom de l’auteur, vendre, par conséquent aussi copier et mettre dans le commerce en leur propre nom, comme une chose qui leur appartient. Mais l'écrit d'un autre est un discours d'une personne (opera), et celui qui l'édite ne peut parler au public qu'au nom de cet autre, et il ne peut dire de lui-même autre chose sinon que l'auteur tient au public le discours suivant par son intermédiaire (impensis bibliopolæ). Il est en effet contradictoire de tenir en son nom un discours qui, d'après son propre avertissement et conformément aux informations du public, doit être le discours d'un autre. La raison pour laquelle les œuvres d'art peuvent être reproduites et livrées au public par d'autres que leurs auteurs, tandis que les livres, qui ont déjà leurs éditeurs, ne peuvent être contrefaits, c'est que les premières sont des œuvres (opera), tandis que les seconds sont des actes (operæ), et que celles-là sont des choses qui existent par elles-mêmes, tandis que ceux-ci n'ont d'existence que dans une personne. C'est pourquoi les derniers appartiennent exclusivement à la personne de l'auteur, et il a un droit inaliénable (jus personalissimum) de parler toujours lui-même par l'intermédiaire de tout autre, c'est-à-dire que personne ne peut tenir le même discours au public autrement qu'en son nom (au nom de l'auteur). Si cependant on modifie le livre d'un autre (si on le raccourcit ou l'augmente, ou si on le refond) de telle sorte qu'il ne serait plus juste de le publier sous le nom de l'auteur de l'original, cette refonte faite par l'éditeur en son propre nom ne constitue pas une contrefaçon, et par conséquent elle n'est pas défendue. Ici, en effet, un autre auteur entreprend par son éditeur une autre affaire que le premier, et par conséquent il ne porte pas atteinte aux droits de celui-ci dans ses affaires avec le public ; il ne représente pas cet auteur, mais un autre, comme parlant par son intermédiaire. De même la traduction d'un ouvrage dans une langue étrangère ne peut passer pour une contrefaçon ; car elle n'est pas le langage même de l'auteur, quoique les pensées puissent être exactement les mêmes.
En gros, de nombreuses pratiquent qu'interdisent les législations et que viennent compenser les Creative Common ne devraient pas être interdites.
Pourquoi les légilsations n'ont pas suivi cette voie ?
Parce qu'elles ne l'ont pas écouté :
Si l'idée, prise ici pour fondement, d'une édition d'un livre en général était bien comprise et traitée (comme je me flatte qu'il est possible de le faire) avec toute l'élégance qu'exige la science du droit romain, les plaintes élevées contre les contrefacteurs pourraient être portées devant les tribunaux, sans qu'il fût nécessaire de solliciter d'abord une nouvelle loi à ce sujet.
et qu'elles ont préférés suivre l'autre alternative, à savoir : solliciter de nouvelles lois à ce sujet. Il est à croire que la complexité législative est le cheval de bataille des États contemporains.
J'avais tenté maladroitement d'aborder ce texte lors des questions au public des dernières RMLL à Beauvais pendant la table ronde avec Véronique Bonnet (de l'April), RMS, une économiste et un juriste qui a publié un livre sur le droit d'auteur sous CC disponible chez framasoft.
Lors de la conférence sur les démêlés entre VLC et Sony sur le blue-ray avec un représentante de la Hadopi, Véronique Bonnet y a à nouveau fait allusion mais sans grand succès. Les libristes n'aiment-ils pas assez la philosophie du droit ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Tu vis sur quelle planète pour pouvoir affirmer ça sans rigoler ?
Sur celle où quand j'entends un morceau avec un thème qui me plaît, je prends ma guitare et je le rejoue à ma sauce : je reproduis la source telle qu'elle m'est donnée. Tu vis sur quelle planète, entouré de quels musiciens, pour avoir entendu des musiciens dire qu'ils se cachaient des choses les uns aux autres ? Je dis ça parce que le mouvement du logiciel libre est né de développeurs qui se plaignaient que d'autres développeurs faisaient de la rétention de code. Tu vois un équivalent dans le domaine musical ?
Et aussi étrange que cela puisse te paraître : j'ai appris comme pour ma langue maternelle, j'ai écouté puis reproduit. T'as pas d'oreille ?
Et alors ? C'est une œuvre de l'esprit, qui répond à un besoin. Partagée, elle répond à des besoins. Libre, elle répond à bien plus de besoins que tout ceux que l'auteur d'origine peut avoir imaginé.
Et alors ? Un théorème mathématique est aussi une œuvre de l'esprit (et avant que la pratique de la démonstration se fasse sous forme de code informatique, tout le monde rendait publique son travail et n'en interdisait pas la réutilisation), mais je n'ai toujours pas vu le rapport avec une œuvre musicale (en dehors du fait qu'ils rentrent tous les deux, comme bien d'autres choses, dans la catégorie générale œuvre de l'esprit); ce qui était pourtant ma question. À ce compte là, tu ferais mieux de militer pour l'abolition du droit d'auteur.
"libre" ? Ben voyons :o
L'usage des chevrons (« ») ne t'a pas fait comprendre que je n'employais pas le mot libre dans l'acception qu'il a dans logiciel libre ? Pourtant la prestation de Bireli aurait pu te mettre la puce à l'oreille : il est là sur la scène devant un public et joue au gré de son inspiration, comme ça lui vient, ce qui s'appelle improviser.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 0.
Pas mieux !
et donc les argumentations diagonales à la Cantor ne s'appliquent pas.
À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.
Maintenant, on constate une technique du genre extension-restriction : le premier stratagème dans l'Art d'avoir toujours raison, avec un soupçon de « je mets de l'eau dans mon vin » sans en avoir l'air.
Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :
Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F…), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.
Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.
à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).
Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.
Sinon, tu devrais en toucher deux mots à Gérard Berry dont les cours des deux dernière années au Collège de France ont été sur les thèmes : Prouver les programmes : pourquoi, quand, comment ? et Structures de données et algorithme pour la vérification formelle.
Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard… perdre du temps est sans doute leur objectif premier.
Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.
Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.
Pour rebondir sur les deux exemples que t'a donné Burps.
Le problème avec
fserait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de typefauxalors que celui-ci est sans constructeur donc vide (ou inhabité).Le second exemple porte un nom de sophisme bien connu : la pétition de principe, le premier étant le raisonnement circulaire qui n'en est qu'une variante. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 2.
Tant que ça ne finit pas comme le théroème de Gödel ou une soirée avec M. Homais, même s'il a lui-même utilisé un argument diagonal à la Cantor. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).
Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Génial
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 3.
Cela est fort possible, je ne connais pas les problématiques d'optimisation liées à l'évaluation paresseuse (dans un terme
(fun x -> une expression avec x) t, on substitue les occurrences dexpar le termetpuis on beta-réduit et on mémoïse pour ne pas avoir à recalculertsi on en a nouveau besoin; là où OCaml commence par évaluer ou beta-réduire le termetavant de substituer puis évaluer le tout). Mais effectivement comme un terme, dans les stratégies paresseuses, se trouve « pris » dans un thunk, cela doit rejoindre sur certains points la différence entre calcul flottant boxé et unboxé en OCaml.Je voulais juste signaler que l'implémentation des optimisations décrites dans la dépêche doit prendre en compte la possibilité d'existence d'effets de bord permis par le langage (comme pour pouvoir propager un terme par exemple), ce qui n'est pas le cas en Haskell.
Il s'agit, il me semble, de deux problématiques d'optimisations orthogonales. D'ailleurs si on fait de l'évaluation paresseuse en OCaml (avec
lazyetLazy.force) cela doit être peu ou pas du tout optimisé, non ?Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1. Dernière modification le 03 mai 2016 à 19:20.
Je l'avais noté dans un coin de ma tête, et je l'ai recherché aujourd'hui. Je m'en suis souvenu car à l'époque (pas si lointaine effectivement, sinon ce serait sans doute sorti de ma mémoire), j'avais fait des recherche pour savoir ce qu'est la SOA et comprendre ta problématique. J'en avais retenu l'idée qu'un WSDL est une façon de décrire la spécification d'un service, et qu'engendrer du code OCaml à partir de cela c'est similaire à de la transpilation.
Quand j'ai regardé encore plus récemment la vidéo de Gérard Berry (vraiment intéressante à regarder, je le conseille si on a le temps : 1h40 avec les questions du public), ça m'a rappelé mes réflexions sur le sujet et comme le sujet du TD est un cas pratique d'un principe plus général qui s'applique aussi à cette situation, je me suis dit : autant le partager.
Pour les problématiques de pédagogie et de didactique, je n'ai pas de réponse non plus, encore moins s'il s'agit d'informatique. La seule discipline que j'ai enseignée, il y a bien des années maintenant, dans le supérieur était les mathématiques; et ce que j'ai retenu de cette expérience est : je suis un bien piètre enseignant. :-/
Cela étant, en ce qui concerne la programmation et l'apprentissage d'un langage, l'approche par la pratique et on aborde les problèmes au fur et à mesure qu'on les rencontre de facto est sans doute moins rébarbatif et plus compréhensible.
Sinon, pourquoi faire de l'inférence de type sur papier ? ça doit être ennuyeux ? Je n'ai rien contre la théorie de la démonstration et la déduction naturelle, mais quand on apprend un langage de programmation ce ne doit pas être la première chose que l'on recherche, non ? Et il y a vraiment des gens qui présentent les tests unitaires en mettant un bouquin de Popper dans les mains de leurs étudiants ?
Sur Popper (j'ai du mal avec son principe de falsification) et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens… :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1. Dernière modification le 03 mai 2016 à 16:00.
Pourtant ce type de TD, et les notions abordées et mises en pratique à travers lui, pourrait t'être fort utile pour développer des bibliothèques qui ne font pas partie de l'écosystème OCaml et dont tu sembles avoir besoin. Je cite cet extrait de ton message de l'époque :
Tu ajoutais que c'est techniquement possible, ce qui est tout à fait vrai et met en pratique les mêmes idées que dans ton transpilateur : voir la conférence de Gerard Berry l'importance des langages en informatique. En particulier, pour le problème concerné, à partir de la 50ème minute1 : « il faut arrêter de penser qu'il y a une syntaxe concrète à un langage, la syntaxe abstraite doit commander : c'est elle la véritable syntaxe du langage. La syntaxe concrète ne doit être qu'une façon commode pour nous de représenter la syntaxe abstraite », suivi de « XML : une syntaxe concrète pour la syntaxe abstraite » et je rajouterai avec information de typage. ;-)
Cette vision du XML constitue aussi, dans un autre domaine, une des originalités de XMPP : les principes à la base des mécanismes de typage dans les langages comme OCaml s'étendent aux protocoles réseau (j'y avais fait allusion dans la discussion qui avait suivi ton message que j'ai cité), et on le retrouve dans la nature même des message échangés dans le fonctionnement d'XMPP. Je n'insinue pas que les concepteurs de XMPP avait cette idée en tête, je n'en sais absolument rien, ils ont peut être simplement fait comme M. Jourdain qui faisait bien de la prose sans le savoir…
cela étant, la totalité de la conférence mérite d'être regardée : elle est très instructive. :-) ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Merci
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 3. Dernière modification le 03 mai 2016 à 12:00.
Je confirme, sa présentation de la problématique était claire avec des exemples illustrant parfaitement les optimisations réalisables, une synthèse avec traduction étant amplement suffisante.
La présentation de Flambda sur le blog de jane street est aussi une lecture intéressante, en particulier sur les exemples choisis : différentes approches au niveau des paradigmes de programmation qui, néanmoins, génèrent le même code.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Génial
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 3.
Les optimisations restent toujours haut niveau. Leur principe est connu depuis longtemps, elles n'étaient juste pas implémentées (ou pas de manière aussi poussée). In fine, ce sont somme toute des opérations élémentaires sur des termes du lambda-calcul : les réduction du l'ambda-calcul (sous-leur noms en apparences ésotériques, la beta-réduction, par exemple, est juste la transformation qui correspond à l'exécution du code, et c'est elle qui est utilisée en partie dans le processus d'inlining).
Contrairement à un langage fonctionnel pur comme Haskell, l'implémentation en OCaml demande plus de soin à cause de la manipulation de valeurs mutables. Mais ils restent encore des optimisations à effectuer, comme les opérations sur les flottants.
Certains auraient même souhaité l'intégration d'« assembleur » inline pour, par example, optimiser le calcul vectoriel en utilisant les jeux d'instuctions SSE.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à -2.
L'intêret de mon commentaire ? Où est le jugement ?
zurvan me dit que 150€ pour un téléphone ce n'est pas la mer à boire. Je lui objecte que ce tarif (pour quelqu'un qui a pas connu le monde antérieur, autrement qu'en tant qu'enfant) a de quoi suscité des interrogations. Et donc je réitère mon propos : où as-tu vu que 150€ pour un téléphone est une dépense standard ? Et tu appelles cela un jugement ?
Mon propos n'est pas de culpabiliser ceux qui peuvent se payer ce type d'outils (je le peux aussi, là n'est pas la question, et je ne me flagelle pas tous les soirs avant de me coucher), ni de dire que libre est synonyme de gratuit, mais de pointer du doigt que 150€ pour un téléphone, cela en fait rire plus d'un (rire surtout jaune).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à 0.
Où est le mépris dans mon propos ? J'aimerais bien qu'on me le signale afin que je puisses adapter mon discours. Peut être n'avons nous pas la même notion du mépris.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à -7.
On ne doit pas côtoyer les mêmes personnes…
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 1.
Je ne suis pas Dieu, je n'ai pas les compétences (telle l'omniscience) pour faire ce genre de chose. ;-)
Sinon, je ne suis pas toujours d'accord en tout point avec l'auteur de l'article qui, bien qu'il s'en défend, fait de la réimportation du fondement de la doctrine libérale (elle trouve ses origines sur notre continent, mais elle a été en partie oubliée, puis elle fût en partie cultivée outre atlantique mais son retour est complètement défiguré).
L'auteur est aussi dans le comité de direction de L'institut Coppet qui est une réédition d'un institut ayant existé à la fin du 18ème et au début du 19ème, dont un des membres originels s'est trouvé pris dans une polémique avec Kant : pour moi, Kant en ressort vainqueur (polémique sur les notions de droits et de devoirs).
C'est fort possible, mais je pense que c'est surtout parce que les questions abordées me sont familières donc ma « lecture » se limite surtout à du déchiffrement de signes alphabétiques.
Pour la promesse que je t'ai faite de réagir sur « vendre du libre », plus la discussion/dispute sur le sujet libre /open source, je crains de ne pouvoir la tenir : entendre par là que mes réponses ne seront pas faites aujourd'hui (je doute d'avoir le temps libre pour cela).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à -7. Dernière modification le 29 avril 2016 à 11:58.
Il n'y a rien qui te choque ?
La réponse à ma question doit se trouver là. ;-)
P.S. : ce n'est pas une question d'android ou non, mais de smartphone = téléphone.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à 1.
C'est pas que je suis opposé à tes propos, sur le fil de la musique libre je te suivais un message sur deux; mais là, je ne comprends même pas ce que tu veux exprimer.
Pourtant je t'ai déjà vu intervenir sur des sujets qui abordés des erreurs de syntaxes et de grammaires, et sur le coup, ta syntaxe m'est incompréhensible : que veux-tu dire ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Support 5 ans vs variantes
Posté par kantien . En réponse à la dépêche Sortie d’Ubuntu 16.04 LTS Xenial Xerus. Évalué à -4.
Ils sont tellement recompilé que sur ma Debian, sans trop jouer l'enfer karmique est du passé (là, si on suit les principes, Debian torche Archelinux les doigts dans le nez), avec les back-ports cela passe pour les novices. Pour le reste, j'attends une meilleure solution.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 4.
Un petit supplément sur le libéralisme : celui qui croit que notre gouvernement actuel cède aux sirènes du libéralisme, que le politique de rigueur est libéral, celui-ci est, pour moi, comme un homme qui croit qu'un hacker est un cracker parce que c'est ce qu'on lui répète à longueur de journée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 2. Dernière modification le 29 avril 2016 à 00:34.
C'est pour cela que j'avais mis un lien ;-) J'ai regardé les tiens, tu aurais pu regarder le mien; d'autant que les tiens sont des vidéos qui représentent 1h30 de temps, là où moi c'était un texte qui se lit en moins de dix minutes. Et tu aurais vu (ou plutôt lu) que les opposants aux mariages gay n'étaient pas ranger dans la catégorie « libéral » par les libéraux eux-mêmes, mais dans la catégorie « conservateur ».
Tu ne peux pas demander à autrui un acte (consulter les liens qu'il te propose et qui font partie de son discours, ce qui n'est rien d'autre qu'une liaison vers une bibliothèque externe) que tu ne fais pas toi même lorsqu'il te répond. ;-)
P.S. : je t'accorde, tout de même, que le terme « libéral » étant tellement galvaudé en France que je suis habitué à ce type de réponse. Le libéralisme n'est pas une doctrine économique, mais une doctrine juridique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 0.
Tu ne serais pas un libéral pur jus par hasard (ce n'est pas un grief sous ma plume) ?
J'ai 2-3 questions à te poser sur la stratégie employée pour faire passer FFV1 auprès des archives autrichiennes, mais ça attendra demain (il y aura peut être du troll sur free / open source, demain c'est trolldi et tu as sacrément tendu la perche, mais je ferai en sorte de faire la part des choses1 ;-)
à moins que tu considères qu'il vaille mieux que je scinde mes propos en deux messages afin de ne pas brouiller inutilement la discussion (ce qui, à bien y réfléchir, est sans doute la meilleure solution). ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: en entreprise
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 1. Dernière modification le 28 avril 2016 à 17:33.
D'ailleurs, n'est-ce pas justement ce qu'il explique dans la première vidéo au sujet du codec FFV1 (vers la 35ème minute) quand l'Archive Nationale Autrichienne a voulu faire des archives sans perte ?
Bien que je n'ai pas tout compris au passage : il compare au choix de la bibliothèque du Congrès (qui a fait un choix propriétaire), puis il dit que les décisionnaires ont décidé d'allouer le budget à une solution propriétaire, pour finir par dire qu'il ont pris ffmpeg et payer pour des fonctionnalités, ce qui leur a coûté bien moins cher, et qu'avec l'argent qu'il restait ils ont pu payer un développeur pour améliorer leur infrastructure. Ils ont réussi à faire changer d'avis les décisionnaires ?
P.S : qui est donc ce lossless Lee ? :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à 5. Dernière modification le 28 avril 2016 à 12:12.
Le problème c'est l'Empire ? Encore un sale coup du côté obscur de la Force !
Je m'en fous, comme droïde de protocoles, j'utilise C-3PO. En plus il peut me traduire toutes les langues connues de la galaxie. \o/
:-D
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mir et Wayland périmés
Posté par kantien . En réponse à la dépêche Sortie d’Ubuntu 16.04 LTS Xenial Xerus. Évalué à 5.
Pour Java, oui, il y en a : je viens à l'instant de mettre à jour open-jdk sur ma Jessie.
De toute façon, un système sans faille de sécurité est un système dans lequel on n'a pas encore trouvé la faille. Rien que depuis le début de l'année chez Debian.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Gnome ?
Posté par kantien . En réponse au journal EVI Smartpad3 , une tablette/ordinateur sous Gnu/Linux. Évalué à 1. Dernière modification le 27 avril 2016 à 21:14.
Pourquoi ? Sur mon portable, je fais le défilement à deux doigts (verticalement ou horizontalement) avec mon touchpad : pourquoi le comportement serait différent sur un écran tactile ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tu pouvais pas mieux tomber
Posté par kantien . En réponse au journal Musique libre, ça vous chante?. Évalué à 3.
Sommaire
Oui, mais ça c'est parce que le système des droits d'auteur actuel est complètement pourri que c'est la croix et la bannière pour faire des œuvres dérivées.
Je vais faire mon kantien, pour une fois, est exposé son point de vue sur la contrefaçon (position prise en 1784 par rapport au problème de la contrefaçon des livres), mais dont les problématiques sont bien encore d'actualité.
Le droit d'auteur relève du droit personnel et non du droit réel
Que puis-je faire avec l'exemplaire d'une œuvre qui est mien ? La propriété de cette exemplaire me donne-t-elle le droit d'en faire une copie et de la livrer au public, ou est-ce attenter à mon droit sur cet exemplaire que de me l'interdire ? Problème actuel : les DRM (cf. note de bas de page graissée).
On retrouve, quinze ans plus tard, dans sa Doctrine du droit les mêmes considérations.
Ce passage se trouve en appendice au chapitre sur le droit des contrats à la question Qu'est-ce qu'un livre ? Le tort du contrefacteur consiste à parler au nom de l'auteur alors qu'il n'a pas été mandaté pour cela : il fait usage d'un droit personnel qu'il n'a tout bonnement pas légitimement acquis (il lui faudrait l'accord explicite de l'auteur pour cela), droit personnel qui ne peut se déduire en toute bonne foi du droit réel qu'il possède sur son propre exemplaire.
C'est sur cette ambiguïté entre droit réel et droit personnel que joue les grands éditeurs pour coller des menottes numériques à tout va. Les DRM porte atteinte au droit réel de l'acquéreur sur son exemplaire qui, de facto, n'a plus la pleine propriété sur son bien : cela mérite plus le terme de contrat de location que celui de contrat de vente. Ce genre de pratique devrait tout bonnement être illégale.
J'avais lu un jour, mais je n'ai pas retrouvé (bon, je n'ai pas cherché très longtemps), un rapport de la quadrature du net pour le Parlement Européen sur le droit d'auteur, et ce qui m'avait surpris c'est qu'il se concentrait uniquement sur le droit réel tout en faisant l'impasse sur le droit personnel : c'est comme s'ils étaient tombés dans le piège des majors en acceptant les termes du débat. Je fût d'autant plus étonné que le rapport était écrit pas des juristes de la quadrature.
Peut-on copier un œuvre artistique, effectuer une traduction ou faire une œuvre dérivée sans le consentement de l'auteur ?
En gros, de nombreuses pratiquent qu'interdisent les législations et que viennent compenser les Creative Common ne devraient pas être interdites.
Pourquoi les légilsations n'ont pas suivi cette voie ?
Parce qu'elles ne l'ont pas écouté :
et qu'elles ont préférés suivre l'autre alternative, à savoir : solliciter de nouvelles lois à ce sujet. Il est à croire que la complexité législative est le cheval de bataille des États contemporains.
J'avais tenté maladroitement d'aborder ce texte lors des questions au public des dernières RMLL à Beauvais pendant la table ronde avec Véronique Bonnet (de l'April), RMS, une économiste et un juriste qui a publié un livre sur le droit d'auteur sous CC disponible chez framasoft.
Lors de la conférence sur les démêlés entre VLC et Sony sur le blue-ray avec un représentante de la Hadopi, Véronique Bonnet y a à nouveau fait allusion mais sans grand succès. Les libristes n'aiment-ils pas assez la philosophie du droit ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tu pouvais pas mieux tomber
Posté par kantien . En réponse au journal Musique libre, ça vous chante?. Évalué à 4. Dernière modification le 26 avril 2016 à 10:42.
Sur celle où quand j'entends un morceau avec un thème qui me plaît, je prends ma guitare et je le rejoue à ma sauce : je reproduis la source telle qu'elle m'est donnée. Tu vis sur quelle planète, entouré de quels musiciens, pour avoir entendu des musiciens dire qu'ils se cachaient des choses les uns aux autres ? Je dis ça parce que le mouvement du logiciel libre est né de développeurs qui se plaignaient que d'autres développeurs faisaient de la rétention de code. Tu vois un équivalent dans le domaine musical ?
Et aussi étrange que cela puisse te paraître : j'ai appris comme pour ma langue maternelle, j'ai écouté puis reproduit. T'as pas d'oreille ?
Et alors ? Un théorème mathématique est aussi une œuvre de l'esprit (et avant que la pratique de la démonstration se fasse sous forme de code informatique, tout le monde rendait publique son travail et n'en interdisait pas la réutilisation), mais je n'ai toujours pas vu le rapport avec une œuvre musicale (en dehors du fait qu'ils rentrent tous les deux, comme bien d'autres choses, dans la catégorie générale œuvre de l'esprit); ce qui était pourtant ma question. À ce compte là, tu ferais mieux de militer pour l'abolition du droit d'auteur.
L'usage des chevrons (« ») ne t'a pas fait comprendre que je n'employais pas le mot libre dans l'acception qu'il a dans logiciel libre ? Pourtant la prestation de Bireli aurait pu te mettre la puce à l'oreille : il est là sur la scène devant un public et joue au gré de son inspiration, comme ça lui vient, ce qui s'appelle improviser.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.