h16

Personne n'a écrit que ça n'existait pas, que c'était exceptionnel ou marginal. Il est même écrit que c'est (malheureusement) banal.

Prix des médicaments : Médecins du Monde utilise la démagogie à doses chevalines RT : https://twitter.com/_h16/status/745151828661149697 http://h16free.com/2016/06/21/54389-prix-des-medicaments-medecins-du-monde-utilise-la-demagogie-a-doses-chevalines

Y'a 30 ans.

Laissons tomber veux-tu. C'est juste pénible et inutile.

On va dire que "c'est confus". D'un côté, il y a tout le PS (députés, notables) qui ont les foies de se prendre une volée de bois vert. De l'autre, il y a Hollande qui tient absolument à conserver le pouvoir, et qui a quelques leviers encore disponibles (je pense que s'il veut, il peut foutre le souk). Bref, si c'est un plan sioux, il doit être alambiqué. Là, ça ressemble plus à un gros "sauve qui peut" indécis. S'il y a plus d'un candidat à gauche (i.e. un vert, un PS hors Hollande, un méluchien ou deux, et donc Hollande en plus de tout ça), la stratégie Hollande de passer le premier tour s'effondre et on risque de se retrouver avec Sarko/Le Pen.

Je ne t'ai pas pris en traitre. 4 fois j'ai clairement expliqué de quoi je parlais. Et le toupet, c'est de ne même pas admettre ça, alors que j'ai tout cité pour qu'il n'y ait pas de doute.

Oui, c'est bien sûr le principal obstacle. Cependant, si les blockchains sont amenées à gérer des montants de plus en plus gros, et laissent aux acteurs la possibilité d'exécuter du code, le rapport coût/bénéfice sera rapidement en faveur de la montée en puissance de ces solutions. Ben c'est comme tout : tant qu'on parle en millions de dollars, ça passe encore et effectivement, les techniques prouvées seront "good enough". Si, un jour, les blockchains gèrent l'argent d'un peu tout le monde (ce que je souhaite et ce qui me semble réaliste), on parlera en trillions, et rapidement, la criticité du système sera supérieure ou égale à celle d'un autopilote d'avion de ligne.

Glisse une vanne ou deux. Excellent test pour savoir si c'est relu.

C'est exploité qq part, ça ?

(je ne suis pas sûr qu'il puisse exister une équivalence : on peut aller de l'un à l'autre mais pas de l'autre à l'un a priori - par analogie, un décompilateur peut produire un source à partir du code machine, mais la sémantique des variables est perdue, par exemple) On en est loin mais pas pour tout. Et Eth est justement l'occasion de mettre en pratique, ou au moins d'apporter un peu de formalisme, d'essayer. Pour le moment, ce n'est pas le cas, et ça n'en prend pas le chemin.

Non toujours pas. Tu peux obtenir des résultats corrects avec cette méthode, ils seront toujours inférieurs à la vérification formelle (par essence) et comme il s'agit d'enlever l'humain le plus possible, le bug bounty en ajoute une trouzaine. Pour la validation, tu ne peux pas utiliser ce procédé non plus puisqu'on n'est pas au même niveau. Mais tout ceci est sans importance, parce que ni toi ni moi ne déciderons de la façon dont ça va se terminer. L'idée est de pointer qu'il existe des systèmes efficaces pour résoudre le problème qui se pose à Ethereum. Ce sont malheureusement des systèmes complexes et pas à la portée du premier venu, et apparemment pas encore dispo pour Ethereum, et donc coûteux. Manifestement, ce ne sera pas ce genre de système qui sera choisi comme solution, et Eth. continuera donc à trainer plus ou moins ce problème. Maintenant, on peut espérer qu'en ajoutant de nouvelles couches d'humains sur des problèmes gérés par des humains pourra venir à bout des soucis. Ca ne s'est jamais produit une seule fois en 60 année d'ingénierie logiciel, mais cette fois, c'est peut-être différent.

Non seulement, j'ai toujours été clair que la discussion portait sur la vérification formelle (et donc pas sur la validation, pas évoquée du tout), mais je l'ai fait à 4 reprises, sans ambiguïté. Du reste, la validation ne correspond pas non plus à ce que tu présentes. La mauvaise foi, ça va deux minutes.

Normalement. Mais bon, ici, on n'est pas IRL, on cherche dont la pureté chimique totale et liborg powa, tout ça, ce qui autorise largement les voyages intergalactiques.

Ceci est une ânerie. Je ne te rabaisse pas, mais le fait que tu le prennes comme ça indique clairement le problème : tu ne veux pas apprendre. Tu considères avoir compris, et tu considères que l'information que je te donne n'est pas utile. Tu ne cherches pas à comprendre cette information, et tu estimes que celle que tu donnes est pertinente (alors qu'elle est juste pile à côté de la plaque). Ceci est une autre ânerie (pas parce que ça ne marche pas - ça ne marche pas, ou pas assez bien comparé à ce que j'évoque), mais parce que c'est encore à côté de la plaque. En substance, tu t'obstines à parler validation, alors qu'on est sur la partie vérification. Et comme tu ne sais pas qu'il y a une différence (fondamentale) entre ces deux concepts, tu t'enferres. Maintenant, tu peux continuer à me balancer du "champion du monde" et autres petites amabilités, ou essayer de voir ce que j'ai voulu dire. A moins bien sûr que tu considères que je suis un imbécile, ce qui expliquerait assez bien ta démarche.

Tu ne comprends pas de quoi il s'agit. Ce que tu viens d'écrire le montre clairement. Il n'y a pas d'humain. C'est tout le but. Ça marche. Ça existe déjà. Renseigne-toi. Allez : https://fr.wikipedia.org/wiki/Notation_Z , https://fr.wikipedia.org/wiki/Méthode_formelle_(informatique) C'est vraiment la base, mais fais un effort.

Le niveau continue de monter, stratosphérique. La galaxie nous appartient. On tutoit l'univers. C'est beau.

En quoi t'ais-je manqué de respect, petite fleur fragile ? Je constate. Si tu comprenais de quoi on parle, tu ne dirais pas "Un moment il faudra bien vérifier formellement et humainement l'outil chargé de vérifier le code", c'est tout. Comme je l'ai écrit, en toutes lettres, de façon compréhensible, "Tout le point est d'éviter l'intervention humaine qui laisse trainer des merdes." (@15:22) ; le but du système proposé est d'autoriser une production de code source à partir d'une description fonctionnelle non ambigüe, sans bug et sans intervention humaine. Si tu rajoutes ensuite : oh bah oui mais il faudra qd même des humains pour vérifier, c'est que tu n'as rien lu ou rien compris.

Le coup du short sur ETH et briber les mineurs, c'est génial.

Bon, tu ne comprends pas de quoi on parle.

Le copain d'Haillèque ?

Tout le point est d'éviter l'intervention humaine qui laisse trainer des merdes. Le groupe d'auditeurs, même payé, face à une vérification formelle, ça fait pas le job. Tu peux payer ce que tu veux, humain = bugs. On a même fait péter des Ariane avec ça. Pourtant, t'inquiète, y'avait de l'incitation et de l'engagement financier.

L'article ne fait pas de critique des script kiddies, il dit à raison que ceux-ci ne sont pas armés pour la tâche qu'ils se sont fixés. Un smart contract est par définition ancré dans le réel. Des specs "en anglais" (en langage humain) sont particulièrement lacunaires ou buguées si on veut (interprétables). L'écart au source pondu est difficile voire impossible à déterminer, le source pondu n'est pas vérifié formellement (au sens mathématique), et le langage choisi ajoute encore en plus des ambiguïtés.

Non et non. Rien à voir. Il existe déjà des systèmes automatiques qui font ça, et c'est tout le point du post du gars. Il y a des domaines où on fait vérifier systématiquement les codes pondus par des outils automatiques, voire on écrit les specs sur ces outils qui pondent un résultat (en C, en ADA par exemple) qui est garanti (sur facture) correspondre aux specs. Il y a par exemple des outils qui vérifient qu'un compilateur pond un code machine qui fera exactement ce qui est décrit dans le code source. Ce n'est pas un humain qui le fait (et qui pourrait de toute façon). Et ce n'est pas trivial, c'est essentiel pour certains systèmes (avionique, par exemple).

mhmmhm dans l'idée, c'est le ML qui permet de vérifier (au sens mathématique) que le code est ok.

Dommage. En ajoutant les illuminatis, tu faisais un sans-faute.