Diagonale de Cantor a écrit 480 commentaires

  • # Autres chaînes de sciences en vrac

    Posté par  (site web personnel) . En réponse au journal Vulgarisation scientifique en vidéo et en français. Évalué à 10. Dernière modification le 31 août 2022 à 10:51.

  • [^] # Re: Limiter l'usage pratique de la CI sans avoir honte de rien

    Posté par  (site web personnel) . En réponse au lien Nouvelle carte d'identité bilingue : l'Académie française prête à saisir le Conseil d'Etat. Évalué à 10.

    C'est fou comme les gens se permettent d'avoir des avis super tranchés sur des choses qu'ils ne connaissent pas.

    1) les racines des mots sont hétérogènes et arbitraires. C'est un peu comme imaginer qu'alterner des mots de plusieurs langues permettait d'en créer une nouvelle: For ejemplo, mélanger English, espanol, et French en la same fraseo…

    C'est vrai qu'une langue qui mélangerait des racines latines, germaniques, grec, etc. Serait forcément moche et ingérable. Euh attends, c'est pas le cas du français et de l'anglais ? La différence de l'espéranto c'est que son initiateur a pris soin de prendre les racines les plus répandue dans le monde occidentale. Par exemple, Europe, mathématique, linguiste ou évangile sont des mots présents et compris dans quasiment toutes les langues européennes. Il n'y aura pas beaucoup d'efforts à faire pour comprendre les mots : Eŭropo, Matematiko, Lingvisto, Evangelio. Et surtout en espéranto la prononciation et l'orthographe sont homogènes, ce qui évite les horreurs de la prononciation anglaise qui n'a quasiment plus rien à voir avec l'écrit.

    2) dans une langue artificielle, il faut forcément une grammaire simple. Où Zamenhof a-t'il pu aller chercher l'idée d'ajouter des déclinaisons? Il picolait ou quoi?

    Pas plus que toi en tout cas : il n'y a pas de déclinaison en espéranto ! Alors tu vas me dire, oui mais il y a un accusatif. Certes, mais il n'y a pas de tableau de déclinaison à apprendre. La lettre finale est toujours « n ». On a la même situation en anglais avec le génitif et la lettre « s »: the teacher’s book. Je ne vois pas en quoi ça rend la grammaire difficile ? D'ailleurs l’anglais a aussi de l'accusatif dans certains cas : I/me he/him she/her à comparer à l'esperanto Mi/Min Li/Lin Ŝi/Ŝin.

    Utiliser une langue existante (la langue de la culture dominante) semble de mon point de vue bien plus pragmatique que d'inventer une langue qui n'existe pas.

    Je comprends que l'on soit contre l'espéranto, ou que l'on considère que l'effort n'en vaut pas la peine, mais il est inutile d'inventer des arguments contre.

    L'espéranto n'a aucune chance de s'imposer pour la même raison que l'on est impuissant face au réchauffement climatique. Après on peut rationaliser cette impuissance comme le renard de la fable de la Fontaine qui déclare que les raisins qu'ils n'arrivaient pas à atteindre sont trop vert. On peut même appeler ça pragmatisme si tu veux, mais ne nous mentons pas. En vrai nous n'avons pas le choix et c'est surtout ça le problème.

  • [^] # Re: Tu es une caricature du client chiant pour le plaisir sadique d'être chiant

    Posté par  (site web personnel) . En réponse au journal Question : Ai-je le droit de refuser d'exécuter un logiciel ?. Évalué à 10.

    Juste par curiosité de savoir si c'est vraiment "Les gens ont le droit de se tromper" et pas essayer maladroitement de cacher le mensonge de GNU, juste dire un fait comme GNU écrit de la merde, peux-tu l'écrire pour confirmer que ta critique est sur la forme de mon commentaire et pas son fond qui ne serait pas compatible avec tes idées?

    Quand j'ai lu la question de Krunch, je l'ai trouvée pertinente (je n'y connais rien, donc cette remarque ne me semblait pas idiote). Et j'ai apprécié le début de ta réponse qui était factuel. Et les faits auraient suffit selon moi à rejeter sa remarque. Même une remarque posée sur le fait que c'est du FUD de GNU aurait été bienvenue.

    Et surtout, même si c'est du FUD déguisé de la part de Krunch et pas une simple question, la virulence de ta réaction est franchement disproportionné. Tu n'as pas l'air de t'en rendre compte…

    Et si on arrêtait de proposer des "alternatives" sans connaître?

    Des fois avoir des questions stupides est intéressant, car tout le monde n'a pas forcément les connaissances sur le sujet (moi par exemple). Donc oui, je ne vois pas le mal à poser une question aussi stupide soit-elle. Ça sert à ça un forum de discussion. Grâce à cette question et grâce à ta réponse, j'ai appris un truc et ça c'est chouette :)

    S'il avait insisté avec mauvaise fois, oui, tu aurais pu être plus virulent (même si c'est loin d'être obligatoire), mais laisse au moins le bénéfice du doute.

    Tu remarqueras que tu es beaucoup critiqué sur la forme, ce qui dommage car sur le fond tes messages sont souvent pertinents.

  • [^] # Re: Tu es une caricature du client chiant pour le plaisir sadique d'être chiant

    Posté par  (site web personnel) . En réponse au journal Question : Ai-je le droit de refuser d'exécuter un logiciel ?. Évalué à 10.

    Mais pourquoi tant d’agressivité !?

    Le message auquel tu réponds est cordial et sous forme de question. C'était de plus son premier message dans la discussion. Une simple réponse factuelle aurait suffit… Les commentaires annexes (« les faits c'est chiant » , « caricature », « fantasme », « blabla ») sont ici inutiles et déplacés.

    Les gens ont le droit de se tromper et on peut leur faire remarquer poliment. D'autant plus que le message initial était respectueux.

  • [^] # Re: l'interview est en pdf

    Posté par  (site web personnel) . En réponse au journal Pour finir ou commencer l'année : une interview de Donald Knuth. Évalué à 10.

    Pire, elle n'a pas été écrite avec TeX !

  • # Débat vs discussion

    Posté par  (site web personnel) . En réponse au journal La cuisine du débat : recettes et récréation. Évalué à 8.

    Ma règle c'est de remplacer les débats par des discussions.

    L'objectif n'est alors plus de convaincre l'autre (ça qui n'arrive quasiment jamais sur le moment, ne serait-ce que pour des raisons d'amour-propre), mais simplement d’échanger nos points de vus: je considère une discussion réussie lorsque j'ai pu me faire comprendre de mon interlocuteur (ce que je pense et pourquoi je pense comme ça) et que j'ai pu le comprendre (pourquoi pense-t-il cela).

    Bref le but n'est plus de gagner mais de clarifier sa propre pensée et aider l'autre en échange à clarifier la sienne. Lorsqu'on y arrive, c'est déjà beaucoup !

    En particulier, dans un débat chacun lance ses arguments en essayant de se débarrasser de ceux de son adversaire. Alors que lors d'une discussion, on pousse au contraire l'autre à développer son point de vue pour réussir à le comprendre. L'autre se sent moins agressé et la discussion est plus paisible. Et souvent on constate que l'autre a de bonne raison de penser ce qu'il pense et on peux lui expliquer qu'ayant eu un autre vécu, on pense différemment.

    Ce n’est pas toujours évident, mais d'expérience, les discussions sont souvent plus enrichissantes que lors d'un débat.

  • [^] # Re: Nous avons de la chance !

    Posté par  (site web personnel) . En réponse au sondage Quel est votre niveau d’anglais ?. Évalué à 10.

    je ne crois pas qu'il y ait des exceptions

    En français ? Une règle sans exceptions ?

    tournesol, parasol, vraisemblable, antisocial, antisymétrique, nanoseconde, etc.

    Voir sur wikiversity

  • [^] # Re: Un volume, des volules ?

    Posté par  (site web personnel) . En réponse à la dépêche Le Frido, livre collaboratif de mathématique de niveau agrégation et un peu plus. Évalué à 2.

    « au lien de volume -> au lieu de volume o:) »
    « au lien de volume → au lieu de volume o:) »

  • # Un volume, des volules ?

    Posté par  (site web personnel) . En réponse à la dépêche Le Frido, livre collaboratif de mathématique de niveau agrégation et un peu plus. Évalué à 4.

    Quand on clique sur les liens de la section Où est‐ce que j’achète ?, on remarque (ce qui me semble être) une typo : dans les noms des liens et sur la page de garde des tomes 2,3 et 4 on trouve volule au lien de volume.

  • [^] # Re: Légende urbaine

    Posté par  (site web personnel) . En réponse au journal 7 faits que j'ai appris cette semaine. Évalué à 7.

    Pour info tu aurais une source, ou est-ce que c'est juste un ami qui te l'a raconté ?

  • [^] # Re: Soit j'ai rien compris soit...

    Posté par  (site web personnel) . En réponse à la dépêche Pijul, contrôle de version et théorie des patchs, version 0.12. Évalué à 2.

    Tu pouvais parler par exemple de OCaml, Haskell, Erlang, des curiosités académiques

    Pour info, Erlang n'est pas du tout académique et provient de l'industrie des télécoms. En pratique et malgré son originalité on sent rapidement des motivations très pragmatiques loin du culte de la pureté théorique.

    Ce n'est pas une critique, car je trouve ce langage absolument géniale, mais pour le coup c'est un mauvais exemple au contraire de ocaml et d'haskell.

    PS : à propos de NixOS quand est-ce que la version 12 de Pijul y sera présente ? Pour l'instant je n'a réussi qu'à installer la version 11.

  • [^] # Re: graphiste stagiaire ?

    Posté par  (site web personnel) . En réponse à la dépêche La norme française de dispositions de clavier a été publiée. Évalué à 6.

    «Donne accès à des lettres grecques, notamment pour la notation scientifique. Par exemple, [μ] suivi de [D] produit Δ.»

    Il me semble qu'il manque des lettres, comme par exemple φ et ψ. Il y a-t-il une raison ?

  • [^] # Re: Timeout

    Posté par  (site web personnel) . En réponse au journal Horodater un cambriolage avec des logs. Évalué à 10.

    Avez tu fais des sauvegardes ?

    Il est toujours délicat de savoir s'il faut tutoyer ou vouvoyer sur Internet…

  • # Un virus belge

    Posté par  (site web personnel) . En réponse au sondage Oui j’avoue, ma plus grosse boulette c’est d’avoir :. Évalué à 10.

    Pour le coup j'étais vraiment petit (j'étais collègien au tout début des années 2000), mais je me suis vraiment senti très très con.

    Le principe du virus belge, c'est que c'est un virus fait par gens qui ne savent pas programmer et qui utilisent donc l'interface chaise-clavier comme interpréteur de commande. Concrètement j'avais reçu un mail, disant quelque chose comme :

    ATTENTION !!! Un virus est en train de se propager sur Internet !!! Pour vérifier si tu es contaminé, va dans tel dossier et regarde si tel fichier existe. Si c'est le cas, supprime le vite !!! Envoie ce mail à tous tes contacts !!! URGENT !!!

    Évidemment le fichier à supprimer était un fichier système très important. C'était sur l'ordinateur de travail de mon père. Le lendemain au boulot il est vraiment passé pour un couillon a devoir expliquer ce que son crétin de fils avait bien pu faire…

  • [^] # Re: Je note...

    Posté par  (site web personnel) . En réponse au journal [HS] Bookmark déplacé : bronsonisation de T411 :<. Évalué à 6.

    Si la loi est mauvaise, il n'y a rien moralement d'incohérent à ne pas la suivre.

    Du moment où tu acceptes que l'autre fasse pareil…

    Et pourquoi ? Si je considère qu'il est bien d'enfreindre la loi pour défendre les droits des noirs, faut-il absolument que je cautionne ceux qui enfreignent la loi pour tuer du noir ? Je ne vois pas le rapport. Tu es en train de me dire qu'à partir du moment où l'on a des valeurs il faut accepter n'importe quelle valeur chez n'importe qui ?

    Tu défends un relativisme extrême dans lequel toutes les valeurs se valent…

    Mais par contre quand une partie non négligeable de la population enfreint la loi sans se sentir moralement coupable, il faut se poser des questions sur la pertinence de la loi. Ça ne veut pas forcément dire qu'il faut changer la loi, mais simplement, qu'une situation en démocratie où la peuple n'est plus en accords avec ses lois est malsaine.

    Le piratage est un symptôme de l’inadéquation de la loi. Mais ce n'est pas la racine du problème, ni sa solution.

  • [^] # Re: Je note...

    Posté par  (site web personnel) . En réponse au journal [HS] Bookmark déplacé : bronsonisation de T411 :<. Évalué à 6.

    C'est certain que comparer l'occupation nazie ou l'apartheid à l'interdiction de se procurer Transformers 3 sans payer les ayant-droits, aucune chance que ça te revienne en pleine face.

    Zenitram dit qu'enfreindre la loi pour suivre son éthique est hypocrite. Je prends un exemple bien célèbre pour montrer que non, pas forcément. On me répond « oui mais c'est différents, là il le fait de manière publique ». Je prends alors l'exemple de la résistance pour montrer qu'enfreindre la loi en cachette pour suivre son éthique n'est pas hypocrite. Alors oui évidemment nous ne vivons pas une période aussi extrême mais ça ne change rien au principe.

    Si la loi est mauvaise, il n'y a rien moralement d'incohérent à ne pas la suivre. Après est-ce que c'est une bonne chose, voilà un autre débat.

    Tout petit j'étais déjà un pirate malgré moi. J'allais sur un site dangereux qui s'appelle la coccinelle.net qui proposait gratuitement les paroles des chansons. Et bien le site avait été fermé par les ayants droits (il a ré-ouvert depuis). Sérieusement ? Quand je traduis à quelqu'un les paroles d'une chanson je suis un pirate ? En quoi ce site faisait du mal au ayant droit ? Défendre les ayants droits c'est défendre des mecs dont la vision du droit d'auteur peut être dans les faits d'ordre quasi fasciste : envoyer un mec en taule parce qu'il a téléchargé 10 chansons, foutre des DRM partout pour avoir un contrôle total sur les œuvres et pouvoir supprimer le fichier quand ils veulent, censurer des vidéos qui vous critiquent, etc.

    Ce n'est pas du tout un acte engagé

    Oui, et ?

    Allons bon. Ils enfreignent la loi pour quoi?

    Simplement parce que la loi est absurde et inadapté ! Faut pas chercher plus loin.

    Il ne faut pas oublier que beaucoup de personnes ont commencé à pirater simplement parce que l'offre légale était inexistante… De nombreuses séries se sont fait connaître en France parce que dès le lendemain on avait le fichier sous titré en français, alors qu'il fallait attendre plusieurs année pour l'avoir en france, si jamais il apparaissait. Et ceci grâce à des passionnés bénévoles qui prenait plaisir à partager.

    La différence entre offre pirate et offre légale ne réside pas seulement dans le prix. L'un offre quelque chose adapté au pratique actuelle et l'autre non. D'autant plus que les gens ont du mal à voir en quoi télécharger une chose qu'il n'aurait jamais acheté par ailleurs pose problème ? L'éthique c'est aussi : pourquoi m'emmerder quand je ne fais rien de mal ? Dire que le piratage entraîne une baisse des dépenses culturelles est un raccourci très rapide.

    Le gros problème est que, indépendamment du prix, l'offre pirate est supérieurs en qualité, en richesse de catalogue, en simplicité ou en absence de DRM à l'offre légale ! Il est là le problème, bien plus que le prix. Je suis parfaitement d'accord que le piratage en l'état n'est pas une solution. D'ailleurs, si tu prends les livres numériques, bizarrement, ceux dont l'offre est sans DRM et avec des prix abordables n'ont pas de soucis de piratage. Étrange…

    Et ça ne pousse en rien les auteurs à produire du contenu Libre.

    Le problème des licences libres est qu'elles légitiment un outil (le droit d'auteur) qui sous sa forme actuelle pose de gros problème. Apprécier la GPL ne signifie pas du tout qu'il faille accepter le droit d'auteur actuel en bloc. Et je ne suis pas sur que les licences libres soit la solution pour tout.

  • [^] # Re: Je note...

    Posté par  (site web personnel) . En réponse au journal [HS] Bookmark déplacé : bronsonisation de T411 :<. Évalué à 6. Dernière modification le 29 juin 2017 à 21:38.

    Note qu'ayant participé à de la désobéissance civile, je sais que son intérêt est dans l’affichage public de ses actes, pas derrière un écran anonyme.

    Donc les résistants de la seconde guerre mondial c'étaient des hypocrites ? Et ne monte pas sur tes grands chevaux en me disant avec des trémolos dans la voix que j'insulte Jean Moulin. Là encore c'est juste un exemple extrême pour montrer l'erreur dans ton raisonnement et non pas pour mettre les « pirates » au même niveau que Jean Moulin ou Martin Luther King.

    Il peut y avoir des cas où des gens choisissent d'enfreindre la loi sans être des hypocrites et certaines formes de piratage/partage en font partie. C'est tout ce que j'affirme ni plus ni moins.

    Je note que tu n'as pas souhaité répondre à mon problème éthique (ton éthique) avec la GPL.

    Parce que ça ne change rien au débat. Un mec peut enfreindre la GPL tout en étant cohérent avec sa morale et alors ? Ça ne rend pas ceci légitime tout comme je n'ai jamais affirmé que les droits d'auteurs ou le piratage (sous sa forme actuelle) était légitime. J'ai juste dit cohérent…

    éthique arbitraire

    Parce que la loi ne l'est pas ? Il est là justement le problème : la loi est du côté de l'éthique de la SACEM (qui est une éthique cohérente), d'aucuns ont un autre éthique du partage (dont tu refuses la cohérence et c'est ce que je te reproche). Il y a débat d'idée et d'éthique. Mais dire que ceux qui enfreignent la loi sont des hypocrites parce qu'ils enfreignent la loi est un mauvais argument. Ils sont sûrement hypocrite mais pour d'autres raisons.

  • [^] # Re: Je note...

    Posté par  (site web personnel) . En réponse au journal [HS] Bookmark déplacé : bronsonisation de T411 :<. Évalué à 10. Dernière modification le 29 juin 2017 à 21:01.

    Ho, je sais bien, quand on veut un truc sans être cohérent sur l'ensemble (…) on trouve toujours une excuse pour dire "moi j'ai l'éthique avec moi".

    Tu est incapable de comprendre que pour les gens il n'y a pas que la loi. La morale a aussi une incidence sur les choix que l'on fait. Tu défends une vision caricaturale dans laquelle il faut soit accepter toutes les lois en bloc soit en accepter aucune. Tu aurais été du genre à expliquer à Martin Luther King que la désobéissance civile qu'il prônait était équivalente à encourager le meurtre ou le viol.

    Et pourtant Martin Luther King était bien cohérent dans sa démarche, mais sa cohérence trouvait sa source dans une autre autorité que la loi.

    Bien sûr, je te l'accorde la désobéissance civile doit rester exceptionnelle et il y a énormément d'hypocrisie à prétendre défendre le partage simplement pour avoir le droit de télécharger le dernier Power Rangers . Mais la piratage ne se résume pas à cela. Pour te donner un exemple, j'ai découvert grâce à t411 plusieurs livre epub que j'ai adoré. J'ai acheté ensuite des livres de ces auteurs. J'ai même racheté un livre simplement pour l'avoir dans ma bibliothèque papier. Je n'ai pas l'impression que mon usage dans ce cas précis pose un problème éthique ou économique.

    C'est cette subtilité que tu semble incapable de voir car pour toi le monde se découpe entre ceux qui respecte les licences et ceux qui les ignorent.

  • [^] # Re: Je note...

    Posté par  (site web personnel) . En réponse au journal [HS] Bookmark déplacé : bronsonisation de T411 :<. Évalué à 10.

    D'un point de vue respect de la loi oui. D'un point de vue éthique du partage non.

    Le droit d'auteur n'est pas un but en soi ; c'est simplement un outil au service de la culture. On peut tout à fais estimer que le droit d'auteur classique à l'heure d'internet est un frein à la culture, en particulier parce qu'il empêche le partage et que la GPL ou autre licence libre est une bonne chose parce qu'elle l'encourage.

    On peut considérer que certaines lois sont néfastes et d'autres bénéfiques sans pour autant être schizophrène. Et bien c'est la même chose pour les licences. :)

  • [^] # Re: Dans le même genre ...

    Posté par  (site web personnel) . En réponse au journal Une charade. Évalué à 10.

    Mon premier est une rondelle de saucisson sur un boomerang
    Mon second est une rondelle de saucisson sur un boomerang
    Mon troisième est une rondelle de saucisson sur un boomerang
    Mon quatrième est une rondelle de saucisson sur un boomerang
    Mon cinquième est une rondelle de saucisson sur un boomerang
    Mon sixième est une rondelle de saucisson sur un boomerang

    Mon tout est une saison

    Réponse : le printemps, car les hirondelles reviennent

  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

    Posté par  (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 5.

    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.

    Pourquoi accuser quelqu'un de mauvaise foi alors que simplement il se pourrait avoir été maladroit dans l'expression de sa pensée ? Dans beaucoup de débat (je préfère le terme de discussion) on se rend compte que finalement l'autre ne pense pas forcément différemment. Le problème est que l'on a naturellement tendance à prouver que l'autre a tort plutôt que d'essayer de le comprendre.

    Qu’on me reproche l'usage un peu rapide de Rice, je veux bien l'admettre mais quand on me dit que c'est complément à côté de la plaque je tente de me défendre.

    Ton message initial auquel je répondais n'était pas non plus dénué de défaut. Tu critiquais l'approche pragmatique en disant qu'elle est dépassable par des approches formels (donc plus mathématiques que empirique). Mais cette critique me semblait étrange dans le sens où pour l'instant l'approche formel est plus ou moins un échec (même si de gros progrès sont fait) et que justement l'approche empirique est une réponse pragmatique à cet échec. Il est évident que l'approche pragmatique est limité, mais le fait qu’en théorie on pourrait peut-être dans le futur faire mieux de manière formel ne me semble pas une critique pertinente de l'approche empirique.

  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

    Posté par  (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 2.

    Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes

    J'ai oublié, d'en parler, le « donc » peut effectivement gêner car il représente un joli raccourci. Est-ce qu'il sera possible un jour d'écrire des programmes complets, concurrent, temps réel en même temps que leur preuve sans que le coût à payer soit trop lourd ? Le théorème de Rice ne le dit effectivement pas, il dit simplement que même pour des propriétés simples (l'absence d'exception à l'exécution) on a même pas de solution simple (répondre à cette question pendant la compilation).

    Alors oui, on pourrait avoir des solutions pas trop moche pour autant, mais pour l'instant on a toujours pas de solution pragmatique simple à l'impossibilité soulevé par le théorème de Rice (comment prouver simplement certaines propriétés importante). Résumer ça en un simple « donc » est effectivement un peu cavalier car ça parle plus d'état de l'art que de résultats théoriques.

  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

    Posté par  (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 3.

    Le problème que nous sommes en train de discuter est de savoir si un programme correspond à sa spécification, elle-même décrite dans un langage fixé. En particulier, on ne regarde pas une propriété fixée sur tous les programmes, mais une propriété différente pour chaque programme.

    Oui, enfin il existe un sous-ensemble de propriétés désirés qui sont les mêmes pour tout les programmes. "Mon programme risque-t-il de planter à l'exécution ?" en est une belle. Et cette propriété peut s'exprimer dans le cadre du théorème de Rice. Soit M une machine de Turing. Le langage reconnu par M est l'ensemble des entrées w pour lesquels m termine sans planter1. Savoir si ce langage est l'ensemble des entrées est indécidable. Dit autrement, conséquence de Rice : un compilateur ne peut pas garantir que ton programme ne plantera pas à l'exécution ni qu'il termine. Donc cela n'a pas "rien à voir". Et c'est ce que je dis depuis le début, on ne peut pas laisser la preuve à un compilateur, on est obligé de se la farcir soi-même.

    Alors certes, tu va me dire que OCaml (si on ne fait que du fonctionnel) permet d'éviter cela. Mais peut-on éviter les débordements de pile avec du typage ? Peut-il empêcher les récurrences infinis ? Peut-il garantir qu'aucune branche ne contenant une exception ne sera jamais atteinte ?

    Je n'ai jamais dis que les preuves de programme était impossible, ni qu’elles étaient inutiles. Ce serait stupide. Mais qu'à priori, elle ne seront jamais suffisante pour garantir l’absence de bug (même si elle permettent d'en limiter un grand nombre). Je serais fort étonné que l'on arrive un jour à passer outre tous les problèmes d'impossibilité avec du typage (puisqu’en fait, tu propose de cacher la démonstration dans le typage). Et quand bien même ce serait possible, alors cela voudrait dire que le système de typage serait devenue bien trop affreux et contraignant pour la majorité des usages.

    Si tu prends ma phrase du début :

    Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes

    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) . Et enfin je n'ai jamais dit que les systèmes de preuves était inutile mais insuffisant. J'ai un peu l'impression que tu me reproche une posture extrême "les preuves en info sont impossibles" alors que depuis le début je parle simplement de la nécessité d'avoir à utiliser des outils complémentaires.

    [1] je sais que le concept de plantage n'existe pas en machine de Turing mais il pourrait se définir sans difficulté aucune.

  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

    Posté par  (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 4.

    Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable. 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.

    et je suis complètement d'accord avec ça. J'espère qu'on est tous les deux d'accord sur le fait que ça n'a pas grand chose à voir avec le théorème de Rice.

    Ben si, car comme je le disais :

    Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif.

    Ainsi de nombreuses propriétés intéressantes ne peuvent pas être prouvée par un compilateur. Alors, oui, certes, sur un programme particulier tu peux faire la démonstration toi même, mais en pratique ça devient vraiment trop lourd. Sans être direct, le lien existe bien. La conséquence concrète de Rice c'est qu'on doit se farcir le boulot (en partie) à la main ; c’est très concret comme résultat.

    Alors certes on pourrait imaginer un outil qui nous aiderai tellement que la partie à faire à la main serait super facile, mais un tel outil n'existe pas. De même que l'on pourrait imaginer des programmes qui permettent de résoudre concrètement des problèmes non polynomiaux car de complexité en o( 10-9999…9999 2n ).

    Se poser la question des conséquences concrètes d'un théorème mathématique est toujours délicat car à notre échelle notre monde n'est pas mathématiques. Même des programmes prouvés formellement peuvent avoir des bugs car ils tournent sur des machines imparfaites. Mais il ne faut pas non plus être trop rigide et accepter quelque imprécision quand on cherche à interpréter concrètement les grands théorèmes.

    Je trouve qu'invoquer Popper et Rice à tour de bras ça fait un peu snob; quand c'est bien employé, pourquoi pas, mais je réagis vite quand c'est mal employé.

    Ben je n'ai pas l'impression que Rice constitue un lieu commun comme Gödel ou la physique quantique. Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque… Pas plus que d'invoquer Popper pour dire prendre un peu de recul et de constater que les tests unitaires ne sont en fait simplement qu’une application des principes des sciences expérimentales à l'informatique.

  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

    Posté par  (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 5.

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

    Je n'ai jamais dis qu'il était impossible de faire des maths ou de prouver des choses, même de manière formel. Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable.

    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.

    Après le problème vient aussi du fait qu'on a privilégié en informatique des langages de goret plutôt que langages propres. Pour un programme purement fonctionnel en OCaml, s'il passe la compilation sans warning on a la preuve qu'on n'aura pas d’erreur de typage à l'exécution et qu'on ne cherchera pas à accéder à des zones mémoires interdites. Dans cette optique par exemples les listes sont très supérieurs au tableau ou l'accès est toujours sources d'erreur potentiel. C'est pareil pour le concurrent, en remplaçant le partage de mémoire par le passage de messages, on a tout de suite moins de problèmes. De même lorsque l'on a remplacé les goto par des while/for/if.

    OCaml donne automatiquement de nombreuses garanties sans que l'on ai besoin de faire les preuves soit même. Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif. Par exemple, le débordement de pile, la terminaison, sont sources d'erreur en OCaml.