gasche a écrit 1151 commentaires

  • [^] # Re: Un an après, qui a changé l'init par défaut ou est passé à une autre distribution ?

    Posté par  . En réponse à la dépêche Debian Jessie, 1 an plus tard. Évalué à 8.

    Pour ma part j'étais passé à Fedora au moment d'installer ma dernière machine parce que j'avais envie de tester systemd pour voir comment c'était en pratique. Je trouve que pour l'utilisateur final l'impact principal c'est plutôt de devoir passer par systemctl (et journald) pour des tâches qui utilisaient d'autres choses avant (/etc/init.d/…), comme relancer un service ou quelque chose comme ça.

    Je trouve toujours que le modèle et l'histoire de Debian sont des références dans le monde du libre, et je pense que je repasserai à Debian à ma prochaine machine. Je me retrouve mieux dans son mode de développement très communautaire—même si je ne me suis moi-même jamais impliqué dans le packaging ou l'évolution de la distribution.

    (Dans une certaine mesure c'est un peu comme Firefox: sur certains points techniques Chromium a l'avantage (en particulier le modèle de sécurité est bien mieux pensé), mais je me retrouve mieux dans les efforts de développement ouverts à la communauté de Mozilla (même s'ils ne s'en sortent pas toujours bien, on a toujours le Pocket un peu en travers de la gorge, etc.), donc à défaut de pouvoir soutenir par une contribution active je l'utilise et j'en parle positive autour de moi.)

    Avec la place de plus en plus importante que prennent les gestionnaires de paquets non-distribution (j'utilise opam pour OCaml par exemple), je défère surtout à ma distribution les parties "chiantes" (les trucs que je veux avoir maintenu et sécurisé, mais pour laquelle à part ça je me moque assez de la version disponible etc.) de mon userland, les trucs qui justent marchent et dont je n'ai pas l'intention de suivre l'upstream. Je pense que mes prochaines aventures d'administration système iront dans le sens de Nix (par dessus Fedora ou Debian), et QubesOS, m'éloignant de plus en plus des distributions classiques.

  • [^] # Re: - pour les distributions

    Posté par  . En réponse à la dépêche Nextcloud, le fork d'ownCloud. Évalué à 10.

    Zenitram, je pense que tout le monde est d'accord pour dire que ce n'est pas super pour l'upstream d'avoir à packager pour toutes les distros. Mais il faut bien comprendre que le coût que ça a et les bénéfices qui y sont associé peuvent rendre cette possibilité plus ou moins importante selon les projets.

    Si je développe un jeu vidéo indie solo, je veux pouvoir distribuer vite mon logiciel aux utilisateurs, et je vais peut-être faire des updates mais pas forcément souvent (et rarement ou jamais des mises à jour de sécurité). Du coup les distros sont très limitantes et un format tout-bundlé est attirant.

    Par contre quand je distribute des services webs qui vont tourner en permanence sur des serveurs et sont sensibles question sécurité (données personnelles de mes utilisateurs, etc.), là la plus-value associée au coût du packaging distro peut devenir vachement plus intéressante. Mes utilisateurs ils veulent pouvoir utiliser leurs outils de sysadmin habituels, leurs canaux habituels quand la n-ième faille dans OpenSSL est découverte, et surtout si chaque fournisseur de logiciel serveur refusait de packager ce serait l'enfer sur terre pour ces utilisateurs.

    Du coup je pense que ton commentaire un peu tout-préparé sur la lourdeur des processus de packaging est moins pertinent ici. Pour OwnCloud, pouvoir utiliser les outils de sa distro est vraiment important pour certaines personnes, pour des raisons qu'on ne peut pas écarter en disant juste "les distros font chier". On peut vouloir améliorer leur processus, essayer faciliter le packaging, les laisser s'en occuper seules et juste faire le minimum pour leur faciliter la vie, râler sur le nombre de distros; mais il y a un vrai besoin qui fait sens dans ce cas.

  • [^] # Re: Merci pour cette annonce

    Posté par  . En réponse à la dépêche Le compilateur GHC Haskell en version 8.0.1. Évalué à 3.

    La différence entre Scala/Clojure et IronPython est que la JVM est leur environnement "natif" (de naissance): tout le monde les utilise sur ça. Pour IronPython, le runtime dotnet est un port alternatif, et il n'a pas beaucoup d'utilisateurs à ma connaissance. Dans l'absolu je suis prêt à acheter que les gens qui ont un soft sur .NET et qui veulent ajouter du scripting en python utiliseraient IronPython: ça semble raisonnable comme choix technique. Mais as-tu des exemples concrets d'adoption ? Pour aller dans ton sens, j'imagine que le fait que c'est le seul des Iron* encore maintenu après que Microsoft ait coupé les fonds est plutôt bon signe. Mais, encore une fois, pour moi il n'y aura un statut d'implémentation alternative "viable" quand quand les gens qui font évoluer le langage prendront en compte aussi les besoins et propositions d'IronPython. (Et à mon avis c'est plus près d'arriver pour Pypy, mais on verra). En tout cas ce n'est pas le cas aujourd'hui.

    La grande majorité des langages réellement utilisés n'ont pas de norme associée à ma connaissance [..] Par contre, il existe des spécifications pour le langage et ce qui doit être considéré comme la bibliothèque standard associée.

    Je suis d'accord, c'est ce que j'ai écrit dans mes messages précédents. Mais est-ce que la référence Python est assez complète pour implémenter une autre implémentation conforme en pratique ? Il me semble que la réponse est non à cause de la dépendance très forte de l'écosystème sur l'interface FFI de CPython, qui n'est pas spécifiée à ce niveau et qui est trop spécifique pour permettre des vraies différences d'implémentation. (Au contraire le travail sur la FFI du projet Pypy a vocation à être portable sur d'autres implémentations, il n'est pas Pypy-spécifique.)

    La plupart de ces langages n'ont qu'une implémentation de référence.

    Encore une fois, tout le monde est d'accord là-dessus. C'est pour ça que j'explique (dans mes messages ci-dessus) qu'il existe des langages vraiment multi-implémentations, mais que Haskell ne l'est plus aujourd'hui—Python ne l'a jamais été, mais ce n'est pas une critique,.

    Notons que dans le cas de IronPython, comme c'est la VM de .Net qui est utilisée, l'implémentation n'est pas forcément mauvaise en termes de perf…

    Ça c'est la théorie. En pratique les VMs pensées pour des langages statiques ont du mal à avoir de vraiment bonnes perfs pour des langages trop dynamiques comme Python ou Ruby (c'est pour ça que MS et Oracle investissent dans le Dynamic Language Runtime, Truffle etc., mais ça reste difficile d'être compétitif). En plus de ça, les programmes Python utilisés en pratique sont plombés par un grand nombre d'appel à C en utilisant une FFI spécifique à CPython et peu portable; dès que l'implémentation alternative, même si elle marche super bien sur du code "Python pur", a un coût de conversion important pour la FFI Cpython, les performances s'écroulent en pratique.

    Par exemple, a-t-on des mesures de quelqu'un ayant récemment fait tourner Django sur IronPython ? Désolé de faire le casse-pieds, mais d'une part je ne suis même pas sûr que ça marche aujourd'hui (enfin s'il y a vraiment des utilisateurs de IronPython ça doit pouvoir se trouver), et d'autre part je m'attends à ce que les performances soient plutôt décevantes.

    Ça n'enlève bien-sûr rien à la potentielle niche de gens voulant ajouter du scripting en Python à leur application .NET. Là les performances sont sans doute moins importantes, et la compatibilité avec les bibliothèques Python existantes non plus. Il n'empêche que je suis sceptique sur la viabilité du pojet à terme si c'est le seul public.

  • [^] # Re: Merci pour cette annonce

    Posté par  . En réponse à la dépêche Le compilateur GHC Haskell en version 8.0.1. Évalué à 3.

    Je suis au courant d'implémentations alternatives de Python (je les mentionne dans mon message ci-dessus), mais je conteste le fait qu'on puisse parler de standard multi-implémentation dans ce cas. Quand tu demandes au gens dans la communauté, la définition de Python c'est "ce que fait CPython". Tu n'as pas:

    • une masse critique qui utilise une autre implémentation que CPython pour lui assurer la longévité en pratique (à part peut-être Jython ?)
    • une tentative d'évolution de l'écosystème pour rendre la vie plus facile aux implémentations alternatives (tout le boulot sur une FFI efficace par exemple doit être tiré à bout de bras par Pypy et Pyston)
    • de discussion saine entre les différents implémentations sur comment faire évoluer le langage (comme c'est le cas pour Javascript ou C++ ou Ada par exemple)
    • ou même une façon raisonnable pour les implémentations alternatives de tester leur conformance comme "une implémentation de Python" (Java, Javascript…)

    Pour moi pour pouvoir parler d'un standard, il faut une définition/description du langage qui soit assez précise pour servir de base à une implémentation (une implémentation n'est pas une description, c'est plutôt un seau de cambouis qui parfois fait des trucs), et que les différents acteurs font des efforts pour respecter. Ce n'est pas une question formelle de normalisation ISO/Oasis/machin (on vu avec ooxml que c'est ouvert aux abus et ça suffit pas), mais une question sociale de la façon dont fonctionne une communauté autour d'un langage. Python (ou Ruby, Perl) n'atteint pas ce niveau; c'est un langage défini par une seule implémentation, avec quelques implémentations alternatives qui courent derrière.

    Et je trouve que mentionner IronPython enlève du poids à ton argument au lieu d'en ajouter. Sérieusement, connais-tu quelqu'un qui a utilisé IronPython pour de vrai, sans avoir été payé par Microsoft pour cela ?

    Quand ils ont lancé .NET, Microsoft avait tout intérêt à montrer sa technologie et à donner l'image d'une plateforme ouverte aux langages qui ne sont pas sous son contrôle direct. Du coup ils ont fait le choix intelligent de financer le développement d'implémentations alternatives de langages à la mode, genre IronPython, ou un backend Scala qui a été mentionné pendant un temps (avant d'être abandonné parce que tout le monde s'en fichait et que ça faisait de la maintenance), etc. (Pour F# c'est différent, les chercheurs avaient envie de se faire plaisir en faisant du ML, ensuite ils ont eu l'idée de faire un clone de OCaml qui était utilisé en interne à MS sur des projets intéressants, et enfin l'équipe Caml leur a conseillé de partir sur un vrai langage à part entière, ce qui a très bien marché.)

    Mais ces backends .NET de langages plus ou moins à la mode (IronPython, IronRuby, IronLisp->IronScheme…) étaient mort-nés: pas de vraie communauté derrière (en plus à l'époque MS ne savait pas vraiment faire du libre), des difficultés sur la compatibilité (pour Python, pas de vrai standard tout ça, trop de code C à porter) ou sur les performances (IronRuby: en fait une VM pensée pour des langages pas trop follement dynamiques a du mal à faire tourner le monkey-patching de façon efficace, etc.). Dans les années 2010, Microsoft a décidé de laisser tomber ces projets qui n'avaient jamais percé, et je ne crois pas qu'ils aient jamais eu une vraie adoption entre temps—les gens mettent du temps à migrer vers des implémentations alternatives, ça va souvent plus vite mais ça marche aussi parfois moins bien, et ça c'est grave.

  • [^] # Re: Merci pour cette annonce

    Posté par  . En réponse à la dépêche Le compilateur GHC Haskell en version 8.0.1. Évalué à 6.

    Dans cette discussion nous utilisons la notion de langage standardisé dans deux sens, un faible (standard sur le papier) et un fort (standard dans les faits):
    - sens faible (sur le papier): il existe une spécification du langage annoncée comme un standard multi-implémentations
    - sens fort (dans les faits): la possibilité d'avoir plusieurs implémentations conformes et compatible est utilisée en pratique, et la communauté est sainement répartie entre plusieurs implémentations

    Python n'est un standard ni sur le papier, ni dans les faits. Il n'y a pas de standard multi-implémentation, la référence du langage évolue en tandem avec l'évolution de l'implémentation principale, Regarde le guide How to contribute to Python sur le site officiel du langage par exemple, il mélange complètement le concept de Python, le langage et CPython, l'implémentation "officielle" (c'est-à-dire, la seule qui définit le langage). Python a une "Language Référence" qui est relativement bien écrite, et pourrait jouer un rôle de spécification, et un processus d'évolution communautaire (les PEPs) bien rodé, mais ça n'en fait pas un langage standardisé.

    (Haskell a un standard sur le papier, Haskell 98, qui a été un standard dans les faits au début (à partir de 1998), mais ne l'est plus aujourd'hui. Haskell est plus standardisé que Python; il a réellement été conçu par un consortium d'implémenteurs de langages paresseux ayant décidé de se mettre d'accord. Les évolutions du langage Python sont décidées par les mainteneurs d'une unique implémentation.)

    Il y a des gens qui travaillent à des implémentations alternatives de Python (Jython, Pypy, Pyston, Stackless Python…), mais celles-ci doivent suivre les choix de l'implémentation principale. En particulier, alors que respecter la sémantique du langage de surface est relativement faisable, être compatible avec la FFI de l'implémentation officielle est très difficile—ce qui limite beaucoup les possibilités de ces implémentations secondaires. On peut se demander si la même situation se serait produite dans un langage standardisé, où plusieurs implémentations sont utilisées dès le départ.

    Pourquoi la standardisation est-elle intéressante pour développer une large communauté ? Parce qu'une infrastructure logicielle, on n'a pas forcément envie de la voir voler en éclat à chaque mise à jour du compilateur.

    Un argument curieux au sein d'une comparaison de Python et Haskell, puisque la communauté Python a un gros problème de fracture entre les versions 2.x et 3.x du langage, alors que la communauté Haskell passe relativement rapidement aux nouvelles versions de GHC.

  • [^] # Re: Merci pour cette annonce

    Posté par  . En réponse à la dépêche Le compilateur GHC Haskell en version 8.0.1. Évalué à 3.

    Peux-tu expliquer en quoi le fait de faire plus de standardisation ferait qu'une "plus large communauté s'y intéresserait (sans doute)" ? Je ne dis pas que je ne suis pas d'accord (je pense que les gens s'intéressent parfois aux choses pour des raisons irrationnelles, et que ça pourrait en effet arriver) mais je me demande si tu as des raisons différentes en tête.

    En tout cas il me semble clair qu'il y a des communautés qui n'ont pas de processus de standardisation et qui ont une communauté très large (beaucoup plus large que Haskell)—par exemple Python, Ruby, Node.js, etc. Il y a aussi des grosses communautés qui sont standardisées et multi-implémentation depuis longtemps (C, C++), mais il me semble que c'est plutôt l'exception que la norme.

  • [^] # Re: Merci pour cette annonce

    Posté par  . En réponse à la dépêche Le compilateur GHC Haskell en version 8.0.1. Évalué à 5.

    Je suis d'accord sur le fait que ce n'est pas vraiment gênant, et que ça peut même un avantage. Je pense que c'est un de ces trucs de communication où les gens ont tendance à imaginer des problèmes où il n'y en a pas, exagérer l'importance de certains trucs "flashy" ou diminuer l'importance de vrais problèmes. À mon avis le mieux dans ces cas-là c'est d'assumer l'état de fait et de contre-communiquer sur ce qu'on trouve important ou intéressant—ta dépêche étant un exemple qui va dans le bon sens.

    Dans l'absolu une implémentation unique peut être problématique. Par exemple, dans le cas où les auteurs de l'implémentation sont soupçonnés de ne pas forcément avoir à cœur l'intérêt commun (par exemple: Oracle avec Java, Microsoft avec leur standard bureautique douteux, Microsoft avec .NET (même s'ils sont particulièrement gentils dernièrement)), quand l'implémentation de référence est propriétaire (DMD pour D, Shen, etc.) ou a des processus de développement trop opaques ou pas assez ouverts (ça fut le cas pour Caml pendant un temps, ça ne l'est plus), ou quand cela réduit la liberté des utilisateurs (les services centralisés qui accumulent les données). Il se trouve qu'aucune de ces critiques ne s'applique à GHC—je pense que le pire qu'on puisse dire de GHC c'est que c'est un vieux, gros projet et que c'est parfois un peu lourd à faire évoluer. Mais une personne qui ne connaît pas bien peut repérer un schéma qui la dérange sans avoir les informations en main pour évaluer si cette craine est justifiée.

    Enfin, il y a des gens qui critiquent légitimement l'abus d'extension chez certains auteurs de code. Les mille-feuilles d'extension, c'est un choix de conception qui vient directement de la monoculture GHC et qui a des avantages et des inconvénients. La raison d'être de fond de cette discussion à mon avis, c'est de créer une pression pour décourager les développeurs d'utiliser trop les extensions avancées du langage, car ça peut rendre le code fragile ou difficile à comprendre pour les néophytes. Il y a des abus, la plupart des gens ont du mal à se retenir de jouer avec leurs jouets, et le fait de râler sur les extensions dans l'absolu peut avoir un effet bénéfique en faisant prendre conscience aux gens que ce n'est pas toujours la meilleure idée.

  • [^] # Re: Merci pour cette annonce

    Posté par  . En réponse à la dépêche Le compilateur GHC Haskell en version 8.0.1. Évalué à 7.

    Je ne suis pas convaincu par ta réponse. Il existe des langages qui ont plusieurs implémentations robustes et utilisées; c'est le cas de C++, avec au moins GCC et Clang, de Javascript (v8, TraceMonkey, Chakra, JavaScriptCore), Scheme, Common Lisp, Prolog. Il existe des langages qui sont mono-implémentation, soit parce qu'ils ont toujours été conçus comme cela, la spécification évolue en tandem avec l'implémentation (OCaml, Python, Ruby, F#, Racket, PHP, Rust, Flash, etc.), soit parce qu'en pratique quasiment tout le monde utilise la même implémentation qui diverge du standard (Haskell, PDF, gmake).

    Cette notion peut évoluer dans le temps; Haskell a commencé comme un langage multi-implémentations (et Hugs reste vaguement utilisable), mais c'est aujourd'hui un langage mono-implémentation dans la pratique. Tu ne peux pas comparer avec C++ comme tu le fais; il y a une différence forte entre "il y a des incompatibilités qui font que toutes les implems ne vont pas gérer tous les projets" et "en pratique le code écrit par les gens aujourd'hui utilise toujours toujours la même implémentation".

    Le processus de standardisation de Haskell est quasiment inexistant aujourd'hui, tous les ans les gens essaient de le relancer et pour l'instant ça n'a pas abouti à grand chose—au mieux une reconnaissance du statu quo avec un nouveau tampon "maintenant c'est standard" sur ce que fait GHC. La communauté Haskell est très vivante, mais pour l'instant c'est avec une implémentation unique; ça pourra re-changer à l'avenir mais ça n'en prend pas le chemin—par exemple il y aurait pu avoir une autre implémentation visant le Javascript, mais en pratique ça ne marche pas bien et GHCJS va sans doute l'emporter.

  • [^] # Re: Destructeurs

    Posté par  . En réponse à la dépêche Crystal, un langage proche de Ruby, en version 0.16. Évalué à 8.

    J'étais en train hier de regarder un article de Phil Wadler, "Linear types can change the world!", qui parle de borrowing et a été écrit en… 1990. Et ce n'était pas le premier article à discuter de ça. L'idée a été implémentée dans Cyclone par exemple ("temporary aliasing of unique pointers"), développé entre 2002 et 2006.

    C'est bien que Rust rende ces idées "mainstream" maintenant mais c'est toujours un peu triste de voir à quel point les communautés de programmation oublient l'histoire des idées dont elles se nourrissent.

  • [^] # Re: Destructeurs

    Posté par  . En réponse à la dépêche Crystal, un langage proche de Ruby, en version 0.16. Évalué à 4.

    Rust ne permet pas d'utiliser un GC aujourd'hui. C'était dans les cartons au début, mais ils ont abandonné l'idée—en 2013, si je me souviens bien. Depuis pknfelix essaie de travailler là-dessus, que ce soit implémenter un bon GC optionnel ou au moins collaborer avec du code extérieur (non-Rust) utilisant un GC, mais c'est vraiment difficile. Cf. cette série de billets de blog récente.

  • [^] # Re: Destructeurs

    Posté par  . En réponse à la dépêche Crystal, un langage proche de Ruby, en version 0.16. Évalué à 2.

    Je pense que tu pourrais faire tout ça avec un très petit nombre d'allocations. D'abord, lire tout le fichier dans un seul grand buffer (tu peux utiliser Buffer si tu ne connais pas la taille à l'avance, ou sinon Bytes). Ensuite, décoder ligne par ligne au lieu d'utiliser input_line, par exemple en utilisant un lexeur. Au final tu as besoin d'allouer au moins une liste pour la sortie, et une chaîne par ligne de sortie (le résultat de decode) si c'est ce que le code utilisateur attend.

    Je pourrais écrire ça si ça rendait service ou permettait de comparer vraiment, à mon avis ce ne serait pas tellement plus long que le code que tu as écrit ici; mais si tu n'as plus l'usage de ce code ce n'est pas forcément la peine. (Si tu en as l'usage, avoir un peu plus d'info sur le format (est-ce que les tailles correspondent au taille des lignes avant ou après pré-processing, ou à autre chose?), et un fichier d'entrée à utiliser pour des tests serait utile.)

  • [^] # Re: Destructeurs

    Posté par  . En réponse à la dépêche Crystal, un langage proche de Ruby, en version 0.16. Évalué à 3.

    Non, je ne crois pas qu'il soit nécessaire de copier de la mémoire à ce moment-là. Il me faudrait une définition plus précise du problème pour pouvoir en dire plus.

  • [^] # Re: Destructeurs

    Posté par  . En réponse à la dépêche Crystal, un langage proche de Ruby, en version 0.16. Évalué à 10.

    Moi je remarque surtout que des langages massivement plus lents que ça sont lourdement utilisés en production (Javascript, Ruby, PHP, Python, etc.), et que les programmes sans gestion automatique de la mémoire sont truffés de faille de sécurité béantes qui nous poussent être mettre à jour nos systèmes à la va-vite chaque semaine. (Oui, on peut faire du code plus sûr en C++ ou Rust (ou même en C macroté) en utilisant du refcounting, mais ça a aussi un coût en performance pas forcément négligeable.)

    Il paraît qu'il reste des domaines applicatifs où les temps de pause des GCs incrémentaux sont inacceptables (enfin bon Azul a montré qu'avec assez d'argent investi dans le problème on peut aller très loin), et tant pis pour eux. Mais sinon tirer en permanence la sonnette d'alarme sur les performances du GC c'est un peu dangereux à mon avis, quand ça pousse les gens à faire des choix techniques qui leurs coûtent au final beaucoup plus cher, en terme de débug ou de failles de sécurité.

    (On va dire que Rust avec ses lifetime c'est magnifique etc. Je pense qu'on n'a pas encore l'expérience pour voir si le code Rust est en pratique plutôt sûr, ou aussi un nid à failles comme C. Le langage fait des bons choix dans la direction de la sûreté, mais une communauté trop portée sur le "unsafe" pourrait faire pencher la balance de l'autre côté, et dans une certaine mesure c'est en train d'arriver. C'est lié aussi au fait que garder statiquement des garanties fortes sur l'ownership c'est en fait assez difficile en dehors des cas simples, quand il y a du partage plus riche, ce qui pousse les gens à faire soit du reference counting (mais les performances, etc.) soit du unsafe.)

  • [^] # Re: Destructeurs

    Posté par  . En réponse à la dépêche Crystal, un langage proche de Ruby, en version 0.16. Évalué à 8.

    Je suis un peu surpris par ton problème.

    D'une part, les strings ont pendant très longtemps été modifiables en OCaml—elles ne sont devenues immutables par défaut qu'en Août 2014, soit sans doute après ton problème, et ça reste une option qu'on peut désactiver. Même avec des strings immutables tu peux toujours utiliser le type Bytes des chaînes modifiables et convertir vers string pour passer à ta fonction de parsing.

    D'autre part, je ne sais pas de quelle fonction de parsing tu parles, mais il me semble que pas mal de lexers/parsers peuvent lire dans un Buffer—peuvent en fait être paramétrés par la fonction qui lit l'entrée. Par exemple le parseur OCaml lit l'entrée interactive du toplevel sans problème.

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

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 4. Dernière modification le 05 mai 2016 à 03:37.

    Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque…

    Le théorème de Rice dit que pour une propriété non-triviale P fixée sur les machines de Turing (exprimée en terme du langage reconnu par la machine), la question de savoir si une machine quelconque vérifie P est indécidable.

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

    Une autre façon de voir que ce théorème ne s'applique pas du tout à ce problème est la suivante: dans les langages avec un système de type correct, le système de typage garantit l'absence de tout une classe d'erreurs pendant l'exécution (typiquement les accès mémoire incorrects, segfault et compagnie): "well-typed programs do not get stuck". Suivant ton raisonnement, le théorème de Rice suggèrerait que c'est impossible—le typeur décide en un temps fini d'accepter ou non le programme, et pourtant il garantit une propriété non-triviale. Mais d'une part on ne part pas de machines de Turing arbitraires, on part de programmes écrits dans un langage conçu pour le typage qui contient des constructions qui guident le typeur, et d'autre part on ne demande pas à décider l'absence de cette classe d'erreur, on se contente d'une sous-approximation correcte (il y a des programmes qui ne sont pas erronés mais qui sont rejetés par le typeur).

    Le fait d'être bien typé peut s'étendre à une notion plus générale de "vérifier une spécification", puisqu'on peut exprimer une spécification comme un type dans certains systèmes—ou choisir de garder ces deux notions séparées, mais la même explication marche pour les spécifications. Bien sûr, plus le système de typage est simple, plus le typeur est facile à écrire—aujourd'hui les outils utilisés pour vérifier les spécifications demandent encore trop d'effort par rapport à ce qu'on voudrait. Mais c'est une question d'interface utilisateur, ça ne correspond pas à une impossibilité théorique venant du théorème de Rice. (Si on veut invoquer un théorème pour justifier la difficulté, il vaudrait mieux partir sur le fait que les preuves sans coupure peuvent être exponentiellement plus larges que des preuves avec, qui explique bien les limitations pratiques d'une partie des approches de démonstration automatique.)

    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.

    Il n'existe pas aujourd'hui (enfin Why3 ou Dafny vont déjà assez loin dans cette direction), mais on y travaille—et le but n'est pas "super facile", mais "au final comparé au temps qu'on aurait passé à débugger, ou aux problèmes causés par les bugs pour ce programme, on y gagne".

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

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 3. Dernière modification le 04 mai 2016 à 17:30.

    Je trouve que les discussions sur LinuxFR sont souvent trop agressives, désagréables et peu accueillantes. Du coup ici j'essaie de faire des efforts pour qu'on ne tombe pas dans le "j'ai dit, tu as dit…", même si mon premier post dans la discussion n'était pas fameux en terme de convivialité—j'ai été un peu dur sur le fait que je trouvais l'utilisation de Rice fumeuse.

    Je pense que quand tu as écrit

    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 [..]

    c'était une mauvaise formulation et tu avais sans doute quelque chose d'autre en tête. Par exemple maintenant tu écris

    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.

    Certes, le théorème de Rice est une exemple notable de résultat formel qui dit que raisonner sur les programmes est difficile. Mon problème avec le fait de l'utiliser dans ce cadre, c'est que tout le monde a l'habitude que quand on s'appuie sur un théorème, c'est pour faire une démonstration qui est formellement valide. Ta première formulation utilise les habits du raisonnement logique ("le théorème dit… donc…"), on pourrait croire que tu veux dire que le théorème de Rice prouve que "les mathématiques ne suffisent pas"—alors que tu as en tête (je suppose après notre discussion) une affirmation empirique sur l'état d'utilisabilité des outils de preuve de programme aujourd'hui.

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

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

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 3.

    On arrive déjà à prouver corrects des programmes non-triviaux aujourd'hui : des compilateurs, des micro-noyaux, des machines virtuelles, des algorithmes concurrents et distribués, des noyaux de navigateur web, et j'en passe. On ne fait pas de la vérification "tout automatique" (qu'est-ce que ce ça veut dire ?), on définit des spécifications et on essaie d'automatiser au maximum la vérification que l'implémentation lui correspond. Le théorème de Rice ne dit rien sur ce qui se passe dans ce cadre, et ça ne semble pas impossible en pratique puisqu'on y arrive déjà (avec plus ou moins d'automatisation), et qu'on améliore constamment les outils pour le faire mieux dans le futur.

    Donc il n'est pas absurde de considérer que la validation de programme relève plus de la science expérimentale que des maths. Et Rice est en partie en cause dans cet état de fait.

    Considérer la validation de programme par une démarche expérimentale n'a rien d'absurde, c'est raisonnable et intéressant. Par contre tu ne peux pas invoquer le théorème de Rice pour justifier que c'est la seule approche possible.

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

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 5.

    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 : et donc là on se tourne vers des méthodes scientifiques, Popper et les tests. Donc oui, quand on peut faire des maths c’est mieux, mais en pratique c'est malheureusement pas possible.

    Le théorème de Rice nous dit qu'un ordinateur ne peut pas décider automatiquement des propriétés non triviales. Ça n'empêche en rien de les prouver avec des mathématiques, ou d'apporter à l'ordinateur des informations supplémentaires (par exemple: une dérivation dans un système de type fixé, ou des invariants et préconditions, etc.) qui rendent le problème décidable.

    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.

  • [^] # Re: première image du site officiel

    Posté par  . En réponse à la dépêche Bilan 2015 du MMORPG Ryzom. Évalué à 7. Dernière modification le 03 mai 2016 à 21:23.

    C'est quand même impressionnant de mauvaise foi comme réponse. Sur l'image, ce qu'on voit en premier (par exemple grâce à un subtil effet de defocus de l'arrière-plan), c'est le cul de la donzelle—et ses épaules. C'est de mauvais goût et il y a beaucoup de gens, en particulier une population de femmes peu représentées dans les jeux vidéos classiques, à qui ça ne fait pas envie.

    Il y a des études de psychologie sur le sujet qui montrent bien un lien entre une exposition à des images sexualisées et des comportements sexistes. Par exemple, dans "Effects of exposure to sex-stereotyped video game characters on tolerance of sexual harassment", Dill, Brown et Collins, 2007, les auteurs montrent qu'exposer des gens à une image à connotation sexuelle issue d'un jeu vidéo (par rapport à un groupe de contrôle à qui on montre une image de femme en habits professionels à son bureau) affecte leurs réponses à un test de tolérance au harcèlement sexuel passé juste après: les hommes ayant été exposés à l'image sexuellement orientée jugent moins souvent qu'une situation relève du harcèlement sexuel. Il y a de nombreuses autres études sur des expériences de ce genre, cf. par exemple les travaux cités par cet article.

    (Je ne pointe pas cette étude du doigt pour dire que les images sexistes poussent les gens à faire du harcèlement. J'ai pris une étude au hasard qui est faite dans un cadre un peu rigoureux sur plusieurs personnes, pour avoir quelque chose de concret à pointer du doigt aux gens qui disent que non, avoir des armures-bikinis ça ne pose aucun problème de sexisme. Apparemment le fait que des dizaines de femmes se soient motivées pour signaler que ça ne leur plaisait pas, créer des blogs entiers dédiés au sujet etc., ça ne leur suffit pas, donc je vais chercher une étude scientifique en espérant que c'est un peu plus concret.)

    Le problème dans ta réponse c'est que c'est la réponse typique qui n'aide en rien, et qui donc aide à persister un statu quo déplorable. Elle n'est pas complètement délirante, au contraire tu utilises des arguments très rationnels pour expliquer que oui, mais bon, peut-on vraiment dire que, bla bla bla. C'est comme ça que se passent toutes les discussions de ce genre: "ah mais veux-tu dire que cette image est sexiste ou sexuée ?". Chaque intervenant dans ces coupages de cheveu en quatre n'est pas forcément mal intentionné, mais ce qu'il s'en dégage c'est un effet d'ensemble où on part d'un constat très simple "mettre en premier sur le site web le screenshot du cul d'une nana, ce n'est pas top", et au lieu d'avoir une réponse productive et efficace du style "oups oui, on va changer pour éviter la gaffe", on se perd dans un labyrinthe d'interrogation existentielles sur ce que c'est vraiment que le sexisme ou une femme discriminée.

    (Ah et je me permets de critiquer le terme de "censure" que tu emploies dans ton message; essayer de proposer de remplacer une image de fesses, ce n'est pas exactement de la censure de l'expression libre.)

  • [^] # Re: première image du site officiel

    Posté par  . En réponse à la dépêche Bilan 2015 du MMORPG Ryzom. Évalué à 7.

    Tu as raison, des femmes peuvent avoir envie de donner une image qui suggère la féminité, et il n'y a rien à dire si c'est leur choix. D'ailleurs il y a aussi des artistes femmes qui créent des représentations genre armure-bikini, pas seulement parce que c'est maintenant (hélas) un standard du genre mais aussi parce que ça leur plaît. Encore une fois c'est très bien.

    Le problème c'est que dans la grande majorité des cas, ce ne sont pas des femmes qui ont fait le choix de cette représentation parce qu'elles s'y retrouvent, mais des hommes qui ont choisit ces images, qui les ont créés ou qui on décidé de les mettre en valeur, et c'est bien par envie (consciente ou non) d'être attiré sexuellement par l'image. Dans la rue tout le monde n'est pas en bikini; dans un jeu vidéo, c'est quasiment inévitable.

    Il y a de nombreuses personnes (femmes ou non) qui expriment leur envie d'avoir d'autres représentations possibles, une image moins stéréotypée dans les jeux vidéos (j'ai donné dans mon autre post des liens vers des blogs entiers de gens qui se plaignent des armures ridiculement peu protectrices des personnages féminins). Je pense qu'il serait bon de les respecter. En tant que créateur de jeu vidéo, d'avoir une vraie diversité de costumes (certains insistants sur la féminité ou la virilité, d'autres non). En tant que diffuseur d'image, en faisant un choix plus réfléchi et moins stéréotypé.

  • [^] # Re: première image du site officiel

    Posté par  . En réponse à la dépêche Bilan 2015 du MMORPG Ryzom. Évalué à 1.

    Tout à fait, cette image est sexiste et devrait être remplacée. Je me suis fait la même réflexion sur l'image "ça y est, tu m'as énervée" de la dépêche: les armures-bikinis c'est assez douteux. Il y a même des sites entiers dédiés à se moquer de ces travers de graphistes.

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

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 5.

    Si ça peut te rassurer, il y a aussi beaucoup de gens qui enseignent C ou Java, et c'est souvent aussi l'horreur pour les étudiants. (Publique statique quoi ?)

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

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 5.

    Ce n'est plus vrai depuis longtemps, dans le sens où les correcteurs des épreuves sont ravis d'avoir des copies écrites en OCaml (je leur ai demandé). Il suffit de le dire aux profs et je pense qu'ils le savent déjà, mais souvent les gens ont la flemme de mettre à jour leurs supports d'enseignement pour utiliser OCaml. J'ai donné des colles en prépa et je laissais mes élèves utiliser le dialecte qu'ils ou elles voulaient.

    La chose qui ne peut pas trop changer c'est le nom du langage utilisé dans le programme officiel (parce que c'est trop difficile de changer un programme officiel, semble-t-il). Damien Doligez a déjà proposé qu'on diffuse la prochaine version de OCaml sous les deux noms "OCaml" et "Caml Light", ce qui serait une façon amusante de contourner. Mais ça n'est pas nécessaire pour commencer à enseigner et utiliser OCaml dès aujourd'hui.

  • [^] # Re: Merci

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 9.

    Tout à fait, une dépêche impressionnante. À ma connaissance ce sont les meilleures notes sur 4.03 qui existent pour l'instant. Est-ce que ça veut dire qu'on devrait les traduire en anglais pour le reste de la communauté ?

  • # Pour quoi connaît-on Turing?

    Posté par  . En réponse à la dépêche A.M. Turing Award 2015 - Cryptographie. Évalué à 10.

    [La récompense "Turing Award"] a été nommée ainsi en mémoire des travaux d’Alan Turing, mathématicien britannique et pionnier dans le domaine de l’informatique, connu pour ses travaux sur Enigma durant la Seconde Guerre mondiale.

    Connu du grand public, ou de la communauté scientifique ? En plus de la cryptanalyse, Turing est surtout connu pour avoir inventé les machines de Turing, l'un des outils de base de la théorie de la calculabilité—et ensuite de la théorie de la complexité.

    (Si on parle de la connaissance auprès du grand public, on peut mentionner aussi son oppression par l'institution britannique à cause de son homosexualité, et son suicide.)