Concernant le premier paragraphe, je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes. Pour citer Xavier Leroy (source):
Csmith has many uses for CompCert, ranging from validating the formal C semantics to finding missing cases and “assertion failed” in the compiler.
Concernant le deuxième paragraphe:
Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses.
Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).
Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.
Juste pour donner mon point de vue: je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante. J'aurais du citer le titre en revanche.
Petite nuance cependant concernant CompCert, puisque le journal laisse entendre qu'il serait infaillible. CompCert n'est infaillible que si l'on suppose ses spécifications correctes, mais rien n'indique que les spécifications sont complètes et réalistes. On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité. Ces dernières années, différents bugs ont été trouvés dans CompCert par test aléatoire (PLDI'11, ISSTA'15, peut-être d'autres, je ne suis pas expert), vraisemblablement causés par des "trous" dans la spécification.
Loin de moi l'idée de remettre en cause l'outil génial qu'est CompCert cependant, juste une nuance :)
Tout dépend ce que l'on appelle désinformation. On pourrait considérer que le manque d'information est une forme de désinformation. En l'occurence, le côté "mielleux, plat et sans intérêt" pourrait être vu comme de la désinformation. Et non, je ne veux pas jeter le bébé avec l'eau du bain. Je n'ai pas de télé physique chez moi, mais il m'arrive de regarder certains extraits via Internet, par exemple si un intervenant m'intéresse. Il y a aussi du bon à la télé, mais on ne va pas se le cacher, ça ne représente qu'un petit pourcentage :) Et en effet, ce n'est pas mieux en soi de s'informer via Youtube ou je ne sais quel site de news "underground". D'où mon:
on tente de ne pas subir la désinformation (et c'est bien plus compliqué que tu ne sembles le croire)
J'ai tout lu. Ca m'a pris une plombe, mais j'ai tout lu. Comme déjà évoqué, la forme détruit complètement le message que tu essayes de faire passer; mais j'ai persévéré.
En bref, rien de neuf sous le soleil. Ta vision "parfaite" et tes réponses au grand mystère de la Vie ne sont qu'un amoncellement de banalités connues du plus grand monde. Bon, à part les 2-3 allusions lézardo-soraliennes qui pointent de-ci de-là. En fait, je me demande si ce n'est pas toi qui regarde trop la télévision. J'ai comme l'impression que tu t'es planté pendant 48h devant ta télé depuis vendredi et que tu te dis "woah, mais les gens croient vraiment ça?". Ben non, on y croit pas, et ça fait bien longtemps que je n'ai pas croisé une télé dans l'appartement d'une connaissance. Nous aussi on réfléchit, nous aussi on s'aime, et nous aussi on tente de ne pas subir la désinformation (et c'est bien plus compliqué que tu ne sembles le croire).
Je ne te ferai pas l'affront de te demander ton âge, mais c'est typiquement le genre de message que j'écrivais du haut de mes 16 ans, à l'époque où j'étais encarté à la LCR et que je coulais 10 douilles par jour. Mais moi aussi je t'aime.
PS: Ce journal n'est pas hors-sujet, une licence libre est évoquée sur la fin.
Je ne suis pas sûr que vous m'ayez compris. Je parle bien de 1% des PdT (matière sèche) = 80kg et 99% des PdT (eau) = 20kg. On a bien 100kg de PdT. Les pourcentages qui sont donnés dans l'énoncé ne concernent pas le poids, ils concernent la composition des PdT ("elles se composent de").
D'ailleurs, sur Wikipedia EN, la formulation est plus précise et élimine le problème:
You have 100 lbs of Martian potatoes, which are 99 percent water by weight.
Et franchement, je ne fais même pas ça pour chercher la petite bête. C'est la manière dont j'ai réagi à la première lecture. J'ai aussi l'impression qu'une partie des énigmes que l'on trouve habituellement jouent sur des formulations alambiquées ou ambiguës.
Il y a bien un truc simple qui doit m'échapper, mais je ne comprends toujours pas la solution à la première énigme. Je ne vois pas comment l'on peut inférer qu'il y a 1kg de matière sèche au départ.
elles (les PdT, pas le poids) se composent de 99 % d'eau et donc 1 % de matière sèche.
Le 1% de matière sèche ne peut-il pas représenter disons 80kg du poids initial?
Si vous remarquez que votre PC ralentit, demandez-vous si vous avez vraiment besoin d’exécuter tous ces programmes et d’avoir toutes ces fenêtres ouvertes en même temps. Au lieu de laisser ouverts vos messages électroniques pour penser à y répondre, essayez de trouver un meilleur pense-bête.
Non mais vraiment, bande d'inconscients, demander du multitâche en 2015! Vous devriez avoir honte!
[^] # Re: Nuance
Posté par Cioran_Naroic . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 1.
Concernant le premier paragraphe, je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes. Pour citer Xavier Leroy (source):
Concernant le deuxième paragraphe:
Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).
Juste pour donner mon point de vue: je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante. J'aurais du citer le titre en revanche.
# Nuance
Posté par Cioran_Naroic . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 6.
Bravo à Mr. Leroy pour ce prix amplement mérité.
Petite nuance cependant concernant CompCert, puisque le journal laisse entendre qu'il serait infaillible. CompCert n'est infaillible que si l'on suppose ses spécifications correctes, mais rien n'indique que les spécifications sont complètes et réalistes. On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité. Ces dernières années, différents bugs ont été trouvés dans CompCert par test aléatoire (PLDI'11, ISSTA'15, peut-être d'autres, je ne suis pas expert), vraisemblablement causés par des "trous" dans la spécification.
Loin de moi l'idée de remettre en cause l'outil génial qu'est CompCert cependant, juste une nuance :)
# Pas sympa
Posté par Cioran_Naroic . En réponse au journal SSH Tron. Évalué à 9.
Non mais j'avais du boulot de prévu moi…
[^] # Re: Android certes, mais Firefox OS
Posté par Cioran_Naroic . En réponse au journal faille Linux 0 day du 19 janvier 2016 . Évalué à 1. Dernière modification le 21 janvier 2016 à 14:05.
Un seul exemple de système démontré sécurisé que tu utilises dans la vie de tous les jours ? Aucun.
[^] # Re: Et ?
Posté par Cioran_Naroic . En réponse au journal Et si l'on pensai ? Enfin je veux dire et si l'on pensai par soi même, ça donnerai quoi ? . Évalué à 6.
Tout dépend ce que l'on appelle désinformation. On pourrait considérer que le manque d'information est une forme de désinformation. En l'occurence, le côté "mielleux, plat et sans intérêt" pourrait être vu comme de la désinformation. Et non, je ne veux pas jeter le bébé avec l'eau du bain. Je n'ai pas de télé physique chez moi, mais il m'arrive de regarder certains extraits via Internet, par exemple si un intervenant m'intéresse. Il y a aussi du bon à la télé, mais on ne va pas se le cacher, ça ne représente qu'un petit pourcentage :) Et en effet, ce n'est pas mieux en soi de s'informer via Youtube ou je ne sais quel site de news "underground". D'où mon:
# Et ?
Posté par Cioran_Naroic . En réponse au journal Et si l'on pensai ? Enfin je veux dire et si l'on pensai par soi même, ça donnerai quoi ? . Évalué à 10.
J'ai tout lu. Ca m'a pris une plombe, mais j'ai tout lu. Comme déjà évoqué, la forme détruit complètement le message que tu essayes de faire passer; mais j'ai persévéré.
En bref, rien de neuf sous le soleil. Ta vision "parfaite" et tes réponses au grand mystère de la Vie ne sont qu'un amoncellement de banalités connues du plus grand monde. Bon, à part les 2-3 allusions lézardo-soraliennes qui pointent de-ci de-là. En fait, je me demande si ce n'est pas toi qui regarde trop la télévision. J'ai comme l'impression que tu t'es planté pendant 48h devant ta télé depuis vendredi et que tu te dis "woah, mais les gens croient vraiment ça?". Ben non, on y croit pas, et ça fait bien longtemps que je n'ai pas croisé une télé dans l'appartement d'une connaissance. Nous aussi on réfléchit, nous aussi on s'aime, et nous aussi on tente de ne pas subir la désinformation (et c'est bien plus compliqué que tu ne sembles le croire).
Je ne te ferai pas l'affront de te demander ton âge, mais c'est typiquement le genre de message que j'écrivais du haut de mes 16 ans, à l'époque où j'étais encarté à la LCR et que je coulais 10 douilles par jour. Mais moi aussi je t'aime.
PS: Ce journal n'est pas hors-sujet, une licence libre est évoquée sur la fin.
[^] # Re: Réponses
Posté par Cioran_Naroic . En réponse au journal Testez votre intuition. Évalué à 2. Dernière modification le 06 août 2015 à 09:38.
Je ne suis pas sûr que vous m'ayez compris. Je parle bien de 1% des PdT (matière sèche) = 80kg et 99% des PdT (eau) = 20kg. On a bien 100kg de PdT. Les pourcentages qui sont donnés dans l'énoncé ne concernent pas le poids, ils concernent la composition des PdT ("elles se composent de").
D'ailleurs, sur Wikipedia EN, la formulation est plus précise et élimine le problème:
Et franchement, je ne fais même pas ça pour chercher la petite bête. C'est la manière dont j'ai réagi à la première lecture. J'ai aussi l'impression qu'une partie des énigmes que l'on trouve habituellement jouent sur des formulations alambiquées ou ambiguës.
[^] # Re: Réponses
Posté par Cioran_Naroic . En réponse au journal Testez votre intuition. Évalué à 1.
Il y a bien un truc simple qui doit m'échapper, mais je ne comprends toujours pas la solution à la première énigme. Je ne vois pas comment l'on peut inférer qu'il y a 1kg de matière sèche au départ.
Le 1% de matière sèche ne peut-il pas représenter disons 80kg du poids initial?
# Le pense-bête papier
Posté par Cioran_Naroic . En réponse au journal Merci Microsoft, ton PC n'est plus superbe. Évalué à 10.
Non mais vraiment, bande d'inconscients, demander du multitâche en 2015! Vous devriez avoir honte!