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
Comme le souligne kantien, il n'est pas clair de savoir ce que tu veux dire par "complètes et réalistes". J'aimerais expliquer pourquoi je me permets de chipoter ici. On a peu de logiciels vérifiés formellement, Compcert est un des premiers qu'on puisse envisager d'utiliser à grande échelle (parce que bon tout le monde n'a pas de raison de faire tourner SeL4 ou CertiKOS sur sa machine, alors qu'un compilateur C si), donc c'est le bon moment de bien comprendre et bien expliquer les garanties (non absolues, bien sûr) données par la vérification formelle. Au grand public, on peut se permettre des approximations et simplifications—encore que. Mais toi tu sembles assez proche du milieu de la recherche pour avoir un avis (foireux) sur comment citer les articles, alors je pense que ça vaut le coup de pousser la discussion un peu plus loin et de te demander d'être précis dans la critique que tu as en tête.
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).
J'aimerais mieux qu'on discute de la question technique sous-jacente (les soi-disant bugs; tu peux essayer de te renseigner mieux, puisque le sujet t'intéresse; moi je me suis renseigné en lisant l'article et j'ai donné mon avis), plutôt que de discuter de on-dit. On n'a pas la réponse précise des auteurs de Compcert, le fait que les auteurs d'un article (qui, même de bonne foi, ont tout intérêt à gonfler l'importance des remarques qu'ils ont fait sur Compcert) disent vaguement "les auteurs sont d'accord" ne veut pas dire grand chose—par exemple si j'étais un auteur poli, ma réponse sur le premier "bug" rapporté serait quelque chose comme "merci beaucoup pour ce retour, je vais effectivement corriger ça, en testant plus strictement les accès aux sous-objets je peux rendre l'interpréteur plus utile", ce qui ne veut pas dire qu'un bug a été trouvé dans Compcert, mais peut être présenté par les auteurs de l'article comme "les auteurs de CompCert sont d'accord et d'ailleurs ont corrigé"—ce qui est faux si on interprète comme tu le fais "sont d'accord" comme "reconnaissent un bug dans Compcert". On est dans l'hypothétique là, et justement j'aimerais en sortir en discutant le fond et pas qui a dit quoi.
Le fait qu'une remarque aux auteurs conduise à un changement dans CompCert ne veut pas du tout dire qu'il y avait un bug à la base. Par exemple le second problème rapporté dans l'article est lié au type de la fonction main, on peut trouver un correctif associé dans le commit 3eb2b3b7bb464, mais la version avant correction respectait tout autant la spécification de correction et compilait tout aussi correctement les programmes valides.
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.
Question de point de vue peut-être, mais qui n'est pas totalement subjective ou arbitraire. En nommant les auteurs je les récompense pour leur travail (puisque la valeur dans le milieu de la recherche n'est pas récompensée financièrement mais par la reconnaissance)—ça me semble très important et juste, et en particulier je préfère toujours citer tous les auteurs et pas "Machin et al.". En nommant la conférence, tu donnes l'impression que la valeur du travail est liée à la réputation de la conférence : les travaux publiés dans une "bonne" conférence sont mis en valeur et ceux qui viennent d'une conférence moins connue sont moins bien considérés. C'est un système qui me semble dommageable, qui encourage la compétition et les mauvaises pratiques—au contraire je préfère que le travail des gens parle de lui-même, qu'on juge l'article par son contenu et pas son étiquette. Après si tu tiens à citer la conférence aussi, rien ne t'en empêche et c'est plutôt la norme, mais le mettre à la place du nom des auteurs me semble mauvais.
(Il faut distinguer de la façon dont les gens citent leur propre travail, par exemple dans leur CV ou leurs exposés de présentation de carrière. Dans ce cas il est courant et compréhensible d'utiliser le format CONF'YY, puisque les auteurs sont toujours l'exposant et ses collaborateurs. Et puis ça correspond à la façon dont beaucoup de gens se souviennent de leurs propres travaux: ils ou elles peuvent avoir plusieurs publications sur la même année et se souviennent souvent bien de l'endroit où chaque travail a été présenté. Mais ça ne se généralise pas nécessairement aux travaux des autres.)
[^] # Re: Nuance
Posté par gasche . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 6.
Comme le souligne kantien, il n'est pas clair de savoir ce que tu veux dire par "complètes et réalistes". J'aimerais expliquer pourquoi je me permets de chipoter ici. On a peu de logiciels vérifiés formellement, Compcert est un des premiers qu'on puisse envisager d'utiliser à grande échelle (parce que bon tout le monde n'a pas de raison de faire tourner SeL4 ou CertiKOS sur sa machine, alors qu'un compilateur C si), donc c'est le bon moment de bien comprendre et bien expliquer les garanties (non absolues, bien sûr) données par la vérification formelle. Au grand public, on peut se permettre des approximations et simplifications—encore que. Mais toi tu sembles assez proche du milieu de la recherche pour avoir un avis (foireux) sur comment citer les articles, alors je pense que ça vaut le coup de pousser la discussion un peu plus loin et de te demander d'être précis dans la critique que tu as en tête.
J'aimerais mieux qu'on discute de la question technique sous-jacente (les soi-disant bugs; tu peux essayer de te renseigner mieux, puisque le sujet t'intéresse; moi je me suis renseigné en lisant l'article et j'ai donné mon avis), plutôt que de discuter de on-dit. On n'a pas la réponse précise des auteurs de Compcert, le fait que les auteurs d'un article (qui, même de bonne foi, ont tout intérêt à gonfler l'importance des remarques qu'ils ont fait sur Compcert) disent vaguement "les auteurs sont d'accord" ne veut pas dire grand chose—par exemple si j'étais un auteur poli, ma réponse sur le premier "bug" rapporté serait quelque chose comme "merci beaucoup pour ce retour, je vais effectivement corriger ça, en testant plus strictement les accès aux sous-objets je peux rendre l'interpréteur plus utile", ce qui ne veut pas dire qu'un bug a été trouvé dans Compcert, mais peut être présenté par les auteurs de l'article comme "les auteurs de CompCert sont d'accord et d'ailleurs ont corrigé"—ce qui est faux si on interprète comme tu le fais "sont d'accord" comme "reconnaissent un bug dans Compcert". On est dans l'hypothétique là, et justement j'aimerais en sortir en discutant le fond et pas qui a dit quoi.
Le fait qu'une remarque aux auteurs conduise à un changement dans CompCert ne veut pas du tout dire qu'il y avait un bug à la base. Par exemple le second problème rapporté dans l'article est lié au type de la fonction
main, on peut trouver un correctif associé dans le commit 3eb2b3b7bb464, mais la version avant correction respectait tout autant la spécification de correction et compilait tout aussi correctement les programmes valides.Question de point de vue peut-être, mais qui n'est pas totalement subjective ou arbitraire. En nommant les auteurs je les récompense pour leur travail (puisque la valeur dans le milieu de la recherche n'est pas récompensée financièrement mais par la reconnaissance)—ça me semble très important et juste, et en particulier je préfère toujours citer tous les auteurs et pas "Machin et al.". En nommant la conférence, tu donnes l'impression que la valeur du travail est liée à la réputation de la conférence : les travaux publiés dans une "bonne" conférence sont mis en valeur et ceux qui viennent d'une conférence moins connue sont moins bien considérés. C'est un système qui me semble dommageable, qui encourage la compétition et les mauvaises pratiques—au contraire je préfère que le travail des gens parle de lui-même, qu'on juge l'article par son contenu et pas son étiquette. Après si tu tiens à citer la conférence aussi, rien ne t'en empêche et c'est plutôt la norme, mais le mettre à la place du nom des auteurs me semble mauvais.
(Il faut distinguer de la façon dont les gens citent leur propre travail, par exemple dans leur CV ou leurs exposés de présentation de carrière. Dans ce cas il est courant et compréhensible d'utiliser le format CONF'YY, puisque les auteurs sont toujours l'exposant et ses collaborateurs. Et puis ça correspond à la façon dont beaucoup de gens se souviennent de leurs propres travaux: ils ou elles peuvent avoir plusieurs publications sur la même année et se souviennent souvent bien de l'endroit où chaque travail a été présenté. Mais ça ne se généralise pas nécessairement aux travaux des autres.)