Je ne suis pas du tout d'accord. Une preuve mécanisée c'est exactement comme du code source; prouver en Coq ou en Isabelle, c'est programmer. Par ailleurs publier un résultat scientifique sans en donner la preuve, c'est extrêmement discutable ne serait-ce que du point de vue de la rigueur et de la méthodologie scientifique.
D'un point de vue de logiciel ça correspondrait à distribuer un exécutable en refusant de donner les sources : tu as le résultat mais pas la façon de faire. On pourrait donc utiliser la même argumentation pour dire que "le code doit exister quelque part mais ne donnera pas plus de valeur à l'application; l'exécutable est suffisant". Je ne suis pas d'accord dans le cas logiciel, je ne suis pas non plus d'accord pour une preuve.
D'ailleurs c'est encore pire parce qu'au moins un logiciel on peut le tester pour vérifier qu'il a bien les fonctionnalités demandées. Ici c'est encore pire parce que sans la preuve on n'a aucune garantie que la preuve a bien été réalisée. À la rigueur ils pourraient dire "on a prouvé" alors que la spec. est inconsistante et on n'aurait aucun moyen de le savoir. On fait confiance aux gens qui le disent donc on ne pense pas ça, mais fondamentalement ça reste un choix de croire les gens aveuglément (sans voir la preuve), ce n'est pas une démarche scientifique respectable.
Je pense qu'on a eu tort d'accepter de publier leur résultat avant qu'ils ne donnent la preuve.
[^] # Re: Avis de Linus Torvalds sur les micro-noyaux
Posté par gasche . En réponse à la dépêche Entretien avec Andrew Tanenbaum à propos de MINIX. Évalué à 7.
Je ne suis pas du tout d'accord. Une preuve mécanisée c'est exactement comme du code source; prouver en Coq ou en Isabelle, c'est programmer. Par ailleurs publier un résultat scientifique sans en donner la preuve, c'est extrêmement discutable ne serait-ce que du point de vue de la rigueur et de la méthodologie scientifique.
D'un point de vue de logiciel ça correspondrait à distribuer un exécutable en refusant de donner les sources : tu as le résultat mais pas la façon de faire. On pourrait donc utiliser la même argumentation pour dire que "le code doit exister quelque part mais ne donnera pas plus de valeur à l'application; l'exécutable est suffisant". Je ne suis pas d'accord dans le cas logiciel, je ne suis pas non plus d'accord pour une preuve.
D'ailleurs c'est encore pire parce qu'au moins un logiciel on peut le tester pour vérifier qu'il a bien les fonctionnalités demandées. Ici c'est encore pire parce que sans la preuve on n'a aucune garantie que la preuve a bien été réalisée. À la rigueur ils pourraient dire "on a prouvé" alors que la spec. est inconsistante et on n'aurait aucun moyen de le savoir. On fait confiance aux gens qui le disent donc on ne pense pas ça, mais fondamentalement ça reste un choix de croire les gens aveuglément (sans voir la preuve), ce n'est pas une démarche scientifique respectable.
Je pense qu'on a eu tort d'accepter de publier leur résultat avant qu'ils ne donnent la preuve.