gasche a écrit 1151 commentaires

Je te remercie pour cette réponse détaillée et nuancée. Je pense que c'est un sujet au final assez compliqué, et je peux comprendre les réactions des créateurs sur certaines questions: ce n'est pas très juste que des plateformes qui proposent d'accéder à leur travail gratuitement se fassent de l'argent en publicité montrée autour de leurs contenus sans leur en reverser une partie.

Je trouve quand même choquante l'idée que des schémas de redistribution des droits, au niveau de la société, puissent se permettre d'ignorer complètement les licences libres utilisées volontairement. Que la SACEM puisse demander des redevances à un supermarché jouant de la musique sous Creative Commons CC-BY-SA, par exemple, me semble profondément choquant et injuste.

J'ai trouvé les supports de cours très bien léchés aussi. Ça a dû demander beaucoup de travail.

Je ne sais pas si tu reçois des notifications de github, mais j'ai fait une (toute petite) pull request.

Oui, et d'ailleurs j'utilise souvent Libreoffice Draw ou Inkscape pour faire des schémas pour des présentations, quel que soit le support de présentation (Beamer, Markdown, etc.).

Jusqu'à présent, en venant de Latex+beamer, j'ai pas trop rencontré de situations où je me suis trouvé limité.

Pour ma part j'utilise une solution à base de markdown (j'utilise pandoc+tzslides pour l'instant, mais remark.js a l'air sympa), mais pour les exposés scientifiques où j'ai besoin de mathématiques je ne peux pas vraiment me passer de LaTeX+Beamer. J'ai fait une présentation en Madoko une fois, il y a un support pour les formules qui est très raisonnable, mais en général je reste sur du Beamer directement—ce qui me permet par exemple de réutiliser facilement des macros que j'utilise déjà dans des articles longs.

As-tu envisagé d'implémenter les listes avec pauses intermédiaires dans Marp directement ? C'est en Coffeescript (berk) plutôt que C++, mais je pense que ce n'est pas forcément très difficile de modifier le code, même si tu ne connais pas déjà le langage, pour ajouter cette fonctionnalité—je commencerais par regarder mds_markdown.coffee. Il me semble que ça rendrait la fonctionnalité beaucoup plus facile à adopter pour les utilisateurs de Marp, au lieu de leur demander de passer par un outil supplémentaire .

Souvent les "goodies" sont des choses dont je n'ai pas vraiment besoin. Dans ce cas, plutôt que de les acheter, je préfère donner de l'argent au projet directement, il récupère plus d'argent — le coût de production en moins. Du coup je trouve l'idée de "pour aider, acheter" pas très convaincante, ce n'est pas la meilleure façon d'aider.

Par contre, et là où votre site prend tout son sens, c'est pour dire : si vous avez besoin d'un tee-shirt, une clé USB, etc., alors vous pouvez l'acheter à travers nous, et vous pourrez en plus soutenir un projet libre (financièrement et par de la publicité indirecte).

Je suis d'accord avec le nom "packager" (empaqueteur ?) plutôt que "maintainer" ici (être mainteneur c'est un rôle upstream), même si les distributions au niveau local parlent de mainteneur pour "mainteneur du paquet".

Je suis encore plus d'accord avec le fait que c'est un bon journal : une tranche de vie bien racontée.

L'auteur aurait peut-être pu mieux montrer que la situation est toujours un peu plus nuancée que ça. Les développeurs de Pale Moon sont peut-être des désagréables de naissance, mais il est raisonnable de supposer qu'ils ou elles n'ont pas commencé comme ça, et qu'il y a des explications à leur indélicatesse. Comme c'est une version de Firefox concentrée sur les performances, il y a sans doute des choix particuliers qui ont été fait sur les versions des bibliothèques externes ou sur les options de build, et une peur que quelqu'un empaquette incorrectement et que des utilisateurs trouvent ensuite le logiciel plus lent ou plus buggué qu'il ne l'est réellement—c'est peut-être déjà arrivé dans ces conditions-là. Ça n'excuse rien, mais ça permet peut-être de comprendre ce qui a mis les gens dans une situation aussi désagréable.

(Je pense que derrière on pourrait réfléchir plus globalement à cette manie de sortir des versions "remasterisées" de logiciels, pour "optimiser" tel ou tel aspect. Mon expérience est que souvent ces projets sont des pertes de temps, qui ne peuvent structurellement rien changer qui n'aurait été possible par un peu de contribution upstream (changer les options par défaut etc.), et qui manquent de la maîtrise technique pour offrir quelque chose de pérenne. Pas mal de temps perdu au final. Bien entendu, c'est souvent plus nuancé que ça, en particulier dans les domaines où la Q/A (Analyse de Qualité) est importante, parce que le comportement global du système est très sensible au fait d'avoir été bien intégré, bien configuré, etc. Ces spin-off "optimisées" jouent alors surtout le rôle d'une distribution clé-en-main, bien testée, pour un certain profil d'utilisateur sur lequel l'upstream ne se concentre pas. Ça a pas mal de sens pour les distributions multimédia par exemple (audio/vidéo, sensibilité aux latences, configuration de Jack, etc.), je suis un peu moins convaincu pour un navigateur web. Mais ce rôle (qui est en réalité un rôle de packaging, configuration et Q/A) permet aussi de comprendre l'état d'esprit des développeurs de Pale Moon et leur résistance à avoir de nouveau paquets downstream. Peut-être se voient-ils plutôt comme des fournisseurs d'un binaire Firefox bien testé pour les systèmes/distributions qu'ils utilisent eux-mêmes.)

Je préfère éviter de discuter d'un langage en particulier dans ce fil de commentaires, car ça me semble un peu hors-sujet (je n'aime pas trop la tendance des discussions sur LinuxFR à se focaliser sur un point très éloigné du journal de départ, et je me suis fait avoir la dernière fois que j'ai essayé de discuter de mon travail à me retrouver dans une discussion interminable sur le langage Go). Quelqu'un a posé la même question pour Python et j'ai créé un topic sur le forum, pourquoi ne créerais-tu pas un autre topic pour discuter de la conception du langage Rust ?

C'est bien ce que j'ai compris (j'ai écrit "vérifié" ci-dessus mais je voulais dire "utilisé", merci LinuxFR de ne pas permettre d'éditer les messages après-coup), et je pense que ce n'est pas vrai.

Je suis très surpris d'apprendre que Coq aurait été vérifié par Villani (je pense que ce n'est pas possible vu son domaine de travail et l'état de la formalisation mécanisée en analyse et en probabilités), je pense que tu as mal compris—mais je n'ai pas accès au livre pour vérifier. Le calcul formel est évidemment utilisé, mais il ne s'agit pas de la même chose (il s'agit d'une aide au calcul, pas d'une vérification des preuves elles-mêmes).

Bon, c'est bien joli de compter les pages de tes articles préférés (ma communauté aussi a des articles longs pour les journaux, même si ça n'est pas toujours très apprécié par les relecteurs), mais tu avais commencé ce fil "Math" avec une discussion un peu plus profonde sur les preuves dans l'activité mathématique (à comparer peut-être avec l'article de 1979 Social Processes and Proofs of Theorems and Programs, très critique de l'idée de preuve mécanisée), et je serais curieux de savoir si cette discussion a dissipé nos différences de point de vue, ou si tu continues à ne pas être convaincu par l'idée que les assistants de preuve pourraient un jour apporter du confort à la pratique de la recherche en mathématiques.

Pour moi le fait que la lecture d'une variable et son écriture se comportent différemment du point de vue de la portée n'a pas de sens (à part "c'est une erreur qui date d'il y a longtemps et on ne pouvait pas la corriger sans risquer de casser du code"), c'est un défaut du langage. Un débutant n'a pas de raison de comprendre pourquoi ça marche dans un cas et pas dans l'autre, et n'a aucune chance de deviner tout seul qu'il faut utiliser nonlocal—en fait personne ne connaît cette fonctionnalité ou presque. C'est un cas typique d'erreur de conception.

Imagine que tu as écris:

def f():
    x = 1
    print(x)

maintenant pour une raison ou une autre, tu veux mettre la dernière ligne de code dans une fonction auxiliaire (et l'appeler pour conserver le même comportement):

def f():
    x = 1
    def g():
        print(x)
    g()

Ça marche très bien, ça fait la même chose. Mais pendant ce temps ton collègue a fait un commit dans son coin, et il a rajouté deux lignes à la fonction de départ:

def f():
    x = 1
    print(x)
    x = 2
    print(x)

Pas de soucis, tu règles le conflit de merge en rajoutant ces lignes dans ta fonction:

def f():
    x = 1
    def g():
        print(x)
        x = 2
        print x
    g()

Et là tu as une erreur UnboundLocalError! Incompréhensible.

Dans un assistant de preuve qui permet aussi de programmer, le fait de pouvoir faire ça est une propriété "émergente" du système, c'est un style de preuve parmi d'autres (preuves par raffinement, par logique de programme, etc.). Par exemple, cette technique est utilisée dans le framework / la bibliothèque Bedrock, conçue pour écrire des programmes bas-niveau vérifiés dans l'assistant de preuve Coq.

Non, et il y a au moins deux raisons :

• C'est plus difficile. Dans le domaine du hardware les domaines d'entrée sont finis (des bus de N bits) et se prêtent très bien à la vérification automatique (grosses formules SAT, etc.). Dans le domaine du software les domaines d'entrées sont plus compliqués ("une URL", "un fichier JPEG"), et les logiques plus compliquées.

• La communauté du hardware est très en avance culturellement à cause du coût des erreurs. La communauté software, et en particulier la communauté du logiciel libre, est en retard sur l'adoption d'outils de vérification.

On commence à avoir des outils pour prouver que deux programmes sont équivalents, mais en général de façon non-automatique. C'est utilisée par exemple comme une façon de faire des preuves de correction : tu écris un programme efficace/optimisé que tu veux utiliser en production, et un programme simple et naïf que tu utilises comme "spécification" (ou implémentation de référence), et tu essaies de montrer qu'ils sont équivalents.

P.S.: Il y a un exception notable, qui est le test d'équivalence entre deux automates. Il y a des outils pour faire ça qui sont utilisés dans certaines communautés (en fait on teste plus souvent le vide, le fait qu'un automate accepte au moins une entrée, mais les deux problèmes sont proches). On peut voir les automates (à état finis, à pile, à poil ras, etc.) comme des cas particuliers de programmes très contraints avec de bonne propriétés—une partie des outils de Model Checking utilise ces idées, par exemple.

Une preuve formelle te donne juste un résultat binaire. Oui la démonstration est juste ou bien Non y'a une merde.
Elle ne t'explique pas l'idée clé. Elle ne te fait pas comprendre intuitivement pourquoi la démonstration fonctionne.

Attention, je ne suis pas d'accord. Une preuve formelle est un document qui décrit la preuve en assez de détails pour être vérifiée par un ordinateur. En particulier, elle contient assez de détails pour être relue et comprise par un humain. Elle n'est pas plus "binaire" en cela qu'une preuve en LaTeX.

La question est de savoir si la personne a fait assez d'efforts, en organisant sa preuve mécanisée, pour que l'argument de preuve soit clair et que la preuve puisse être comprise. (Un programme informatique aussi peut être "correct", faire ce qu'on attend, mais illisible par un autre humain. Une preuve LaTeX aussi peut être incompréhensible.)

Aujourd'hui les outils que nous utilisons pour écrire les preuves mécanisées gênent un peu pour écrire des preuves vraiment agréables à relire—d'où l'habitude de maintenir aussi une preuve informelle en LaTeX en parallèle. On travaille à améliorer cela aussi, et aujourd'hui il est déjà possible en faisant des efforts (de la part de l'auteur, surtout, mais aussi du lecteur) de présenter des preuves mécanisées qui sont aussi lisibles/compréhensibles.

(Je pense que tu as en tête une image des preuves vérifiées basées seulement sur la démonstration automatique, où on demande à l'ordinateur de reconstruire l'argument de preuve sans aucune information (le SAT/SMT-solving par exemple). Quand on utilise un assistant de preuve, on peut (et on doit) donner les arguments de preuve à l'assistant, dès qu'on veut démontrer des propriétés plus complexes/intéressantes que ce qui est facile à vérifier par une machine.)

L'idée n'est pas de remplacer le document décrivant la preuve par le code de la preuve mécanisée, mais de le complémenter. Aujourd'hui la preuve LaTeX a deux rôles, à la fois communiquer le résultat et s'assurer, du mieux possible, qu'il n'y a pas d'erreurs. C'est agréable quand on est un lecteur qui sait que la preuve a déjà été acceptée par la communauté et qui peut se concentrer sur la compréhension, mais pas pour :

• les premiers rapporteurs/relecteurs, qui ont une lourde responsabilité vis-à-vis de la communauté et à qui la partie "re-vérifier les calculs et les arguments" peut demander énormément de travail (en plus du travail de compréhension d'ensemble, etc.)
• l'auteur lui-même, qui n'a pas d'outils adapté pour, par exemple, savoir quelles parties du développement doivent être revues si il ou elle modifie une définition ou change une hypothèse

(Un exemple un peu extrême est la démonstration proposée de la conjecture ABC, qui a été proposée à la communauté en 2012 et dont on ne sait toujours pas si elle acceptée ou pas.)

Quand on utilise un assistant de preuve, les rapporteurs/reviewers doivent d'une part comprendre l'argument d'ensemble (comme avant) et les idées des preuves (comme avant). Pour savoir si les preuves sont correctes dans les détails, il suffit de lire les énoncés de la preuve mécanisée, et de se convaincre qu'ils correspondent effectivement aux énoncés de l'article informel (il peut bien sûr y avoir des erreurs à ce niveau-là); re-vérifier indépendamment la preuve mécanisée est ensuite "immédiat" (on fait tourner le programme vérificateur de preuve), et donne une confiance très forte dans la validité de la démonstration. Ça aide aussi beaucoup l'auteur en cas de modification de la preuve au cours de son écriture.

Une partie de ma communauté travaille déjà comme ça : dans certaines de nos conférences il y a un tiers (je dirais, à la louche) des soumissions qui viennent avec, en complément, une preuve mécanisée, et cela nous a permis d'attaquer des problèmes plus difficiles et de faire des raisonnements plus techniques avec confiance, et en gardant des temps de revue/relecture relativement courts (quelques mois).

(C'est aussi absolument nécessaire pour la preuve de programmes, où on écrit une preuve mathématique du fait qu'un programme correspond à une spécification. La nature très calculatoire de certaines parties de ces arguments fait qu'il est extrêmement pénible de relire les détails des preuves pour un humain, et que le risque d'erreur d'inattention augmente beaucoup.)

Un exemple typique est le livre "Homotopy Type Theory", qui a été entièrement formalisé avec un assistant de preuve (en Agda), en parallèle avec la rédaction du livre dans un style "informel" (non vérifié) mathématique classique.

C'est de façon générale quelque chose de très demandé et étudié, on peut espérer du progrès à ce niveau (c'est également nécessaire pour augmenter les perfs).

Oui, ou alors on peut aussi utiliser dès le départ un langage typé et plus performant.

(Il y a un côté ironique à voir plein de gens utiliser un langage pour faire quelque chose pour lequel il n'a pas été conçu au départ, se rendre compte que ça coince, et se mettre à tous dire en groupe : « on est tellement nombreux à avoir des ennuis, quelqu'un va bien finir par nous sortir du fossé ».)

Ce qui donne envie aux gens d'étudier la théorie d'un langage, ce n'est pas le fait qu'il ait beaucoup de fonctionnalités différentes. Ça c'est plutôt repoussant, au contraire. C'est le fait qu'on puisse regarder des fonctionnalités originales, qui n'existent pas dans d'autres langages et n'ont pas été étudiées, et apportent soit une grande expressivité soit donne des propriétés intéressantes au langage. Pour Perl6, si quelqu'un voulait l'étudier, je ne sais pas trop ce qu'il faudrait regarder. Quelles sont ses fonctionnalités uniques ?

Les grammaires Perl6 sont intéressantes, mais on a déjà des langages de grammaires extensibles, et il n'est pas forcément clair de trouver des problèmes difficiles à résoudre dans ce domaine. Les hyper-opérateurs sont rigolos, mais ces idées existent déjà dans les langages à tableaux qui sont étudiés (et plus simples que Perl6 donc plus attirants pour se concentrer sur cette fonctionnalité), voir le travail sur Remora par exemple. Enfin, il y aurait peut-être les jonctions, qui sont amusantes aussi, mais je dirais que c'est plus du travail de linguistique (donner une explication du comportement attendu des expressions exprimées avec des jonctions en terme d'opérations plus simples). Je pense que si je voulais travailler sur Perl6 je choisirais les jonctions : comment leur donner un sens de manière la plus générale possible, en évitant les exceptions et cas particuliers ?

Ça n'a pas vraiment de sens sur ce contexte de dire "l'INRIA pousse ci plutôt que ça"; personne ne nous a demandé de travailler sur tel ou tel langage, c'est chaque chercheur qui choisit le domaine qui lui paraît le plus intéressant ou motivant pour ses recherches. Il y a un peu de pilotage de la recherche dans un institut (par le choix des recrutements) et au niveau national (par le choix des financements), mais c'est à un niveau bien plus grossier ("plus de machine learning et de bio-informatique à tel endroit", "renforcer la cryptographie ici") que le choix d'un langage parmi d'autres.

Une des premières visites que j'ai faites cette année c'est à l'équipe RMOD à Lille, qui travaille sur le langage Pharo, un des héritiers de Smalltalk et Squeak les plus actifs. De l'autre côté, à Sophia-Antipolis, Manuel Serrano travaille sur Hop, un langage multi-tiers sur le web, maintenant un dialecte de Javascript mais utilisant son implémentation de Scheme. Une partie de l'équipe Celtique à Rennes travaille sur la formalisation de programmes Javascript. Il y a de la recherche en langages dynamiques à l'INRIA.

C'est un peu hors-sujet alors j'ai créé un topic ailleurs pour en discuter: De la conception du langage Python.

Et tu n'as pas parlé d'une partie qui me semble prendre de plus en plus de temps dans le monde académique : la recherche de financement. Est-ce parce que l'INRIA est protecteur de ce point de vue, parce que c'est une partie négligeable dans ton cas, autre ?

Je suis jeune chercheur; je n'ai pas encore cherché à encadrer des étudiants pour un stage rémunéré ou surtout une thèse, donc je n'ai pas eu de besoin direct de financement. C'est quelque chose que je découvrirai dans les années à venir.

Mes seules sources de dépenses pour l'instant (à part le salaire) sont les voyages. Je voyage pas mal dans le cadre de mon travail (pour rendre visite à des équipes de recherche à qui expliquer mon travail, assister à des conférences internationales, etc.). L'INRIA fournit à mon équipe un budget pour cela, et je suis relativement bien loti. Pour 2018 je peux dépenser environ 3000€ en voyages, ce qui convient si on est raisonnable; c'est plus que d'autres collègues en France (ou encore plus qu'en Amérique du Sud, en Grèce, etc.), mais moins que les gens qui ont obtenu des financements complémentaires. En comparaison, une conférence d'une semaine aux États-Unis au moins $2200.

Tu dis que ta communauté est en contact avec celle qui poussent des langages comme Julia. Concrètement, comment se passent vos échanges, sur quels types de questions vous penchez vous etc ? Êtes-vous en contact avec la communauté LLVM pour aller vers des transformations prouvées, faire évoluer l'IR etc ?

J'ai des collègues qui ont travaillé sur le fait de comprendre la relation de "sous-typage" de Julia (voir ce résumé d'exposé), qui est utilisée pour résoudre les appels de fonction (multi-method dispatch). Cette relation était définie assez vaguement dans la documentation, et il y a une implémentation de référence qui est compliquée (c'est une partie qui a évolué avec le temps et pleine d'optimisations variées). Ils et elles ont trouvé des aspects non-intuitifs de cette implémentation, certains qui sont des bugs qui ont été corrigés par les implémenteurs du langage, certains qui sont des difficultés de conception qui demanderaient des évolutions du langage, ou à prendre en compte pour un nouveau langage de ce genre. Les discussions se font souvent par email, parfois en direct (une partie de ces collègues est à Boston, et une partie des développeurs Julia aussi), et portent sur des questions précises (tel comportement est-il intentionnel ou bien un bug ?) ou sur des questions plus générales (voici comment on comprend/modélise ceci ou cela, est-ce que ça correspond à votre intuition / votre implémentation ?). Ce n'est pas toujours évident de discuter parce que les connaissances de chacun peuvent être très différentes—les développeurs de Julia ne connaissent pas forcément bien le typage, même si leur langage l'utilise en fait de façon fondamentale.

Êtes-vous en contact avec la communauté LLVM pour aller vers des transformations prouvées

Oui, voir par exemple Provably Correct Peephole Optimizations with Alive, Nuno P. Lopes, David Menendez, Santosh Nagarakatte et John Regehr, 2015.

(Techniquement ces chercheurs sont dans une communauté un petit plus éloignée de la mienne, plus orientée "compilation" et "vérification automatique" que "sémantique des langages de programmation" et "typage"—mais ce sont des proches qui discutent beaucoup ensemble.)

Ce n'est pas facile parce que les développeurs de LLVM s'intéressent peu aux méthodes formelles et, en général, à la correction de leurs passes (l'idée d'ensemble est que si ça passe dans la testsuite, c'est raisonnable), mais il y a eu un gros travail de discussion/sensibilisation sur ces dernières années (un des chercheurs sur ce travail, Nuno Lopes, contribute maintenant régulièrement au code, et ça aide), donc ça progresse petit à petit.

faire évoluer l'IR (LLVM) etc ?

Oui, Taming Undefined Behavior in LLVM, Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, Nuno P. Lopes, 2017.

La grande majorité des langages de programmation permettent d'écrire des choses que quelqu'un qui ne connaît pas le langage trouvera difficile à lire. (Ceux qui ne le permettent pas sont jugés trop verbeux.). Je ne pense pas que cet exemple montre que OCaml est plus "abscons" qu'un autre langage dans l'absolu, mais plutôt que tu n'es pas déjà habitué à sa syntaxe.

En l'occurrence, il s'agit d'un filtrage de motif:

• { row = []; _ } est un motif qui teste si la valeur observée est un bien un enregistrement ({ ... }) (record en OCaml, un type produit avec des champs nommés, comme une struct en C) avec un champ row contenant la liste vide (row = []) et potentiellement d'autres champs ; _. Il se trouve que ce record est défini dans le module Varsets, d'où le Varsets. pour qualifier.
• (Negative [] | Positive Varsets.{ row = []; _ }) est un motif qui filtre une entrée de type (Varsets.row, Row.row) signed, c'est-à-dire soit une valeur de la forme Positive foo où foo est une liste (c'est la définition de Row.row), ou une valeur de la forme Negative bar où bar est de type Varsets.row (l'enregistrement). Ce motif-ci accepte soit la liste vide dans le cas Negative, soit un Varsets.row dont le champ row est la liste vide dans le cas Positive — donc une ligne vide, qu'elle soit positive ou négative.
• (Negative [] | Positive Varsets.{ row = []; _ }) :: _ est un motif de liste (p :: q filtre une liste chaînée dont le premier élément filtre p et la suite filtre q), qui filtre une liste dont le premier élément est une ligne vide (positive ou négative), et la suite n'importe pas.

La ligne de code complète dit donc que si on prend en entrée une matrice dont la première ligne est vide (positive ou négative), alors on fait un assert false: cette fonction ne doit être appelée que sur des matrices dont la première ligne est non-vide. Les clauses suivantes du filtrages vont donc pouvoir gérer le cas où la première colonne est négative non-vide (Negative (n :: ns)) ou positive non-vide (Positive Varsets.{ row = p::ps; varsets; }).

Il semblerait que le problème principal soit le côté symbiotique art+code de notre projet. Certaines personnes nous ont ainsi dit explicitement qu'elles ne veulent pas nous financer car elles s'intéressent à GIMP mais pas à un film d'animation (apparemment si je faisais un financement pour le développement seulement, j'aurais plus, ce qui m'attriste !).

C'est très étonnant comme réticence, je trouve, mais ça suggère une solution simple : pourquoi ne pas aussi ouvrir une source de financement en ton nom propre, au titre du développement de Gimp seulement ? Tu pourrais soit parler uniquement de la partie "film d'animation" dans l'espace ZeMarmot, soit parler des améliorations de Gimp dans tes retours d'information sur les deux financements. Je pense que personne ne verrait de problème à ça : les gens qui veulent financer seulement le code donneraient sur ton "compte de développeur Gimp", ceux qui veulent financer les deux (et Artyom aussi) donneraient sur ZeMarmot.

Ce que je trouve spectaculaire dans cette histoire c'est à quel point leur erreur magistrale était facile à éviter. Aujourd'hui tout le monde parle de A/B testing, c'est quand même assez évident de se dire que, avant d'annoncer à tous ses utilisateurs un changement de la façon dont les frais sont calculés (question assez centrale sur une plateforme de mécenat), il serait bon de commencer par interroger 1000 créateurs et 1000 utilisateurs au hasard pour leur demander ce qu'ils en pensent, et ce qu'ils feraient si les frais étaient changés de cette façon. Patreon annonce "We messed up", et je pense que c'est vrai, mais pas sur ce qu'ils disent : on ne sait pas si leurs nouveaux calcul des frais était une erreur (ils ont des raisons à discuter), mais par contre leur conduite du changement était exécrable et ça c'est une erreur bien plus importante.

Un autre projet de nouveau shell intéressant est Oil Shell, dont le créateur communique beaucoup et très bien (en anglais), par exemple sur son blog. Certaines idées me semblent assez déraisonnables (l'auteur a implémenté son propre système de build et créé un fork de Python pour y écrire son projet), mais c'est rigolo et intéressant à suivre.