Thomas Douillard a écrit 9166 commentaires

Les comparaisons ont leurs limite mais ça n'empêche pas qu'il y ait des points communs.

Déja parce que la frontière est parfois floue, cf. le non brevetage des brevets logiciels contournés par l'adjonction de procédés matériels. Un bon exemple serait la googlecar. La bidouillabilité du logiciel de la googlecar serait une bonne chose ?

Ensuite parce que des trucs comme la faille Heartbleed montrent qu'on a parfois qu'une illusion de contrôle de ses données personnelles grâce aux logiciels libres. Le logiciel est libre donc auditable. Est-il audité pour autant ? Il a fallu deux ans pour trouver la faille. On peut très bien utiliser toute une stack de logiciels libre, c'est très loin d'être une garantie qu'on contrôle effectivement tout …

Et alors ?

Faudrait faire de l'IA sur le corpus légal et modéliser dans un formalisme logique les lois pour tester leur cohérences et détecter les incohérences potentielles. Mais c'est pas sans problèmes, le corpus est gigantesque, il faut modéliser les zones grises …

N'importe quoi, c'est une étude forcément partielle, comme toute les études. Ils concluent en donnant la suite des recherches à accomplir, c'est une démarche normale et saine, pas une constatation qu'ils ont fait une étude foireuse.

“Given that users who receive no feedback post less frequently, a potentially effective strategy could be to ignore undesired behaviour and provide no feedback at all,”
CQFD.

C'est fatigant de vivre avec ce genre d'état d'esprit. Tu peux faire confiance à personne sauf à un groupe d'amis très restreints, les autres te veulent potentiellement du mal. Si un de tes amis fait un pet de travers, il est éjecté du cercle. Pour rentrer dans le cercle, il faut faire preuve de ta fiabilité.

C'est valable à différente échelle : tu peux faire un peu plus confiance aux gens qui raisonnent plus ou moins comme toi (une histoire "d'identité" ?)

Vous envisagez de créer des trucs genre des exports ou en json ou en RDF (format quelquonque) des données, genre pour les utiliser plus facilement hors de python et créer des APIs qui les utilisent dans d'autre langages ? Ça pourrait quasi être réinjecté dans un serveur web.

En ignorant les problèmes de licence, ça peut être une extension cool.

J'ai du mal à croire que quelqu'un qui raisonne en terme de systémie propose de rédiger un plan B à l'échelle Européenne sans vraiment chercher à sortir de France. Je crois pas que son initiative de rédiger un texte de l'époque ait vraiment amené quelque chose, mais de base c'est absolument pas crédible de pas penser cette rédaction à l'échelle des Européens et pas uniquement des français.

Bonjour, le journal est un peu ancien, je te conseillerai d'en poster un nouveau sur le sujet avec des éclairages de quelqu'un qu'y s'y connait, ça aurait sans doute plus de visibilité :)

Au pif, un cribblage "in vivo" ou par éprouvette c'est un tri des molécules avec des vraies molécules en essayant d'identifier celles qui s'apparient à la molécule "requête", "in silico" c'est la même chose avec des modèles de molécules informatiques des molécules ?

N'importe quoi, free ils en ont fait autant pour le web fermé non ? À moins que tu considère leur bras de fer avec google comme un combat contre l'impérialisme des DRMs … Bon, ils hébergent Linuxfr, c'est sympa, après …

En même temps se baser sur un comportement très probablement non spécifié et qui consiste à rajouter un timeout relativement long pour une appli, et non garanti, c'est le genre de truc qui arrive que ça casse. (oui, le français de cette phrase est déplorable).

Gnome 2 était très bon dans le genre aussi en fait.

Je savais pas que Randall Munroe avait publié un xkcd graph generator, non plus. C'est quoi l'url ?

Que les devs soient payés n'implique pas vraiment qu'ils aient beaucoup plus de comptes à te rendre. Je suis plutôt content qu'ils aient de l'argents pour pérenniser un peu leurs efforts, Firefox face à Chrome, Gimp face à Photoshop, aussi bien Firefox que Gimp ne jouent pas dans la même cour au niveau moyen que Google ou Adobe.

Euh, moi je vois surtout des gens qui s'estiment super mauvais en anglais, je vois pas en quoi le constat est nié.

Et on s'arrête au constat ? Si on s'arrête là on a aucune solution.

Oui et non, l'approche de la méthode B c'est d'écrire des specs et de vérifier que l'implémentation respecte bien les specs, et au passage qu'il n'y a pas de bug à la con comme des buffer overflow. Après comme toujours les specs ont des limites, on peut pas vérifier la cohérence d'un protocole cryptographique si on code seulement un client et un serveur indépendament en B. Ni que la précondition P=NP qui serait l'hypothétique garantie de la sécurité du protocole en question, mais on c'est pas parce qu'on fait du B qu'on est obligé d'essayer :) ~~~~

Pas du tout, si j'ai bien compris le principe de la faille, elle permet d'accéder à une zone mémoire qui ne devrait tout simplement pas être accessible. C'est pas une bête histoire de borne ?

Je parle pas vraiment de faire de la preuve de protocole, en fait, on dialogue de sourd.

Bien sur que si, déja si on peut garantir qu'il n'y a pas de bug d'implémentation type heartbleed c'est pas mal. Ça démontrera pas la totale correction du protocole c'est sur. À part ça, j'ai vu passer un récent ajout de modélisation système pour la méthode B sur l'article Wikipédia, je sais pas ce que ça recouvre et j'ai pas investigué, mais si ça se trouve ils s'intéressent à certaines problématiques de distribution.

Pour revenir a des choses plus terre à terre, la faille qui a provoqué tout ça elle n'a pas un nombre arbitraire de pairs et il s'agissait juste d'une erreur de validation des IOs :) On peut prouver des choses rien qu'en bétonnant les IO, évidemment c'est plus compliqué de valider Internet dans sa globalité.

TEDLT

La spec, dans la méthode B, elle est haut niveau au début du developpement et elle se précise au fur et à mesure (c'est le raffinage) justqu'à devenir compilable. Les trous dans la spec tu les détectes parce que c'est impossible de montrer que ton raffinage est compatible avec ce que tu as écris avant. Ils mettent le processus de spec et de preuve au coeur du développement.

C'est dur de prouver des systèmes distribués, certes, mais écrire du code correct et être sûr qu'il est correct c'est carrément ultra dur aussi. Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.