Je crois bien que le ton de nos échanges est monté par ma faute, j'en suis désolé. J'étais mal luné l'autre jour, j'aurais du tourner mes doigts dix fois avant d'écrire, j'en suis désolé. :-/
Le bug peut être également dans le model.
Tout à fait, mais cette problématique est hors de portée de la logique et des approches formelles.
Cette partie de la logique de notre connaissance peut donc être nommée analytique, et elle est la pierre de touche, du moins négative, de la vérité, puisqu'il faut d'abord contrôler et estimer d'après ces règles toute connaissance selon sa forme, avant de l'examiner selon le contenu pour établir si, à l'égard de l'objet, elle contient une vérité positive. Mais, comme la simple forme connaissance, aussi d'accord qu'elle puisse être avec les lois logiques, ne suffit (nullement) pour établir la vérité matérielle (objective) de la connaissance, personne ne peut se hasarder de juger des objets avec la simple logique, et à en affirmer quelque chose, sans en avoir entrepris auparavant une étude approfondie en dehors de la logique, pour ensuite essayer simplement de les utiliser et de les lier en un tout cohérent selon les lois logiques, mieux encore, des les examiner simplement d'après elle. Cependant, il y a quelques choses de séduisant dans la possession d'un art aussi spécieux, celui de donner à toute nos connaissances la forme de l'entendement, quelque vide et pauvre qu'on puisse être à l'égard de leur contenu, que l'on use de cette logique générale, qui est simplement un canon pour l'évaluation, comme d'un organon pour produire réellement, du moins en en donnant l'illusion, des affirmations objectives, ce qui est en fait abuser de cette logique.
Kant, Critique de la Raison Pure.
La partie graissée correspond à ce que tu dis : si l'erreur est dans le modèle (le contenu, la matière), la logique qui ne s'occupe que de la forme ne peut rien y faire. Pour grossir le trait, la logique n'a rien à reprocher au raisonnement suivant :
les hommes sont immortels
or je suis un homme
donc je suis un immortel
celui qui se croirait immortel, en se justifiant du fait que la logique ne trouve rien à redire à ce syllogisme, ferait rire n'importe qui face à lui. :-D
Pour faire une analogie avec le domaine juridique : la logique s'occupe des vices de forme dans la procédure. En l'absence de vice de forme, il faut tout de même un procès pour débattre de l'issue du cas : on y examine la question de droit (la majeure du raisonnement : les hommes sont immortels) et la question de fait (la mineure du raisonnement : je suis un homme). Ici, la majeure est en tort : l'accusé est innocenté, déclaré non coupable, ou plutôt non immortel. La question de fait en revanche ne fait ici pas de doute; en cas de non lieu c'est celle-ci qui n'a pu être justifiée.
J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
Tout à fait : c'est bien pour cela que je parlais d'un travail de titan ! Il faut formaliser les instructions assembleurs (de trois architectures qui plus est : PowerPc, ARM et x86), formaliser la sémantique d'un sous-ensemble assez large du C, puis prouver que toutes les transformations-traductions du code préservent les sémantiques. Mais Xavier Leroy et son équipe on pu réaliser cet exploit (car s'en est un, une première au monde pour un compilateur) parce qu'ils avaient déjà un forte expérience dans l'écriture de compilateur et de sémantique des langages de programmation : ils en avaient entrepris auparavant une étude approfondie en dehors de la logique. ;-)
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
Nulle condescendance dans mon message, je mets cette réaction sur le dos du ton que prenaient nos échanges. Je ne suis pas sans savoir comment cette question est gérée en l'absence d'un tel outil, mais je tiens à signaler que la garantie que CompCert apporte sera à jamais inaccessible à ces méthodes. Raison pour laquelle Gérard Berry, qui n'ignore pas non plus ces méthodes, a écrit :
Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.
Le graissage est de moi pour bien souligner que les méthodes auxquelles tu fais allusion, si elle sont acceptées en pratique, ne pourront jamais apporter ce niveau de garanti (j'espère que tu m'épargneras un débat épistémologique sur la distinction entre la connaissance rationnelle et la connaissance expérimentale afin de justifier cette position).
Je tiens à préciser à nouveau que ce compilateur fait partie de la chaîne d'outils que AbsInt vend à ses clients dont Airbus. :
Check your C code for runtime errors with Astrée.
Compile the code using CompCert
Check your stack usage with StackAnalyzer
Analyze the execution time with aiT
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier.
Bien sûr que j'ai le compris : un tel outil doit savoir cacher ses entrailles pour exposer à l'utilisateur ses concepts métiers pour qu'il se focalise sur ce qu'il connaît. Il n'empêche que sous le capot, c'est de la traduction mathématique et de la preuve mathématique, quand bien même l'utilisateur n'en a pas conscience. Un bon outil est celui qui sait se faire discret sur son fonctionnement : celui qui l'utilise, celui qui le construit et celui qui le répare sont rarement les mêmes personnes, n'ont pas les même savoir, ni les mêmes compétences.
D'ailleurs pour illustrer la chose : je ne connaissais pas Go, si ce n'est de nom. Résultat je suis allé jeter un coup d'œil, et bien je trouve leurs choix tout sauf bêtes contrairement à ce que certains ont pu dire. Il n'y a certes pas de généricité (sauf sur quelques types comme les tuples ou les tableaux) mais leur système de type interface est très ingénieux et semble compenser allègrement à l'usage l'absence de généricité. D'un point de vue formel, au premier abord (je n'ai pas creusé plus que cela) ça s'apparente grandement à des fonctions avec arguments implicites sur du lambda-calcul simplement typé avec enregistrements (un langage avec des fonctions comme citoyen de première classe pour lequel un argument de certaines fonctions est inférer par le compilateur)1. Le polymorphisme au lieu d'être paramétrique (comme C++, Java, Haskell...) et ad-hoc mais vérifier à la compilation. Choix qui offre aux développeurs un large panel de technique de programmation sans l'assomer avec des abstractions difficiles à comprendre, donc à maîtriser et donc à utiliser (comme le sont les modules ou les GADT pour toi).
Haskell a cela avec ses type classes, mais OCaml manque d'un tel dispositif ce qui rend un code qui fait un usage intensif de modules très vite incompréhensible pour celui qui n'en est pas l'auteur. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
Je crois bien que le ton de nos échanges est monté par ma faute, j'en suis désolé. J'étais mal luné l'autre jour, j'aurais du tourner mes doigts dix fois avant d'écrire, j'en suis désolé. :-/
Tout à fait, mais cette problématique est hors de portée de la logique et des approches formelles.
La partie graissée correspond à ce que tu dis : si l'erreur est dans le modèle (le contenu, la matière), la logique qui ne s'occupe que de la forme ne peut rien y faire. Pour grossir le trait, la logique n'a rien à reprocher au raisonnement suivant :
celui qui se croirait immortel, en se justifiant du fait que la logique ne trouve rien à redire à ce syllogisme, ferait rire n'importe qui face à lui. :-D
Pour faire une analogie avec le domaine juridique : la logique s'occupe des vices de forme dans la procédure. En l'absence de vice de forme, il faut tout de même un procès pour débattre de l'issue du cas : on y examine la question de droit (la majeure du raisonnement : les hommes sont immortels) et la question de fait (la mineure du raisonnement : je suis un homme). Ici, la majeure est en tort : l'accusé est innocenté, déclaré non coupable, ou plutôt non immortel. La question de fait en revanche ne fait ici pas de doute; en cas de non lieu c'est celle-ci qui n'a pu être justifiée.
Tout à fait : c'est bien pour cela que je parlais d'un travail de titan ! Il faut formaliser les instructions assembleurs (de trois architectures qui plus est : PowerPc, ARM et x86), formaliser la sémantique d'un sous-ensemble assez large du C, puis prouver que toutes les transformations-traductions du code préservent les sémantiques. Mais Xavier Leroy et son équipe on pu réaliser cet exploit (car s'en est un, une première au monde pour un compilateur) parce qu'ils avaient déjà un forte expérience dans l'écriture de compilateur et de sémantique des langages de programmation : ils en avaient entrepris auparavant une étude approfondie en dehors de la logique. ;-)
Nulle condescendance dans mon message, je mets cette réaction sur le dos du ton que prenaient nos échanges. Je ne suis pas sans savoir comment cette question est gérée en l'absence d'un tel outil, mais je tiens à signaler que la garantie que CompCert apporte sera à jamais inaccessible à ces méthodes. Raison pour laquelle Gérard Berry, qui n'ignore pas non plus ces méthodes, a écrit :
Le graissage est de moi pour bien souligner que les méthodes auxquelles tu fais allusion, si elle sont acceptées en pratique, ne pourront jamais apporter ce niveau de garanti (j'espère que tu m'épargneras un débat épistémologique sur la distinction entre la connaissance rationnelle et la connaissance expérimentale afin de justifier cette position).
Je tiens à préciser à nouveau que ce compilateur fait partie de la chaîne d'outils que AbsInt vend à ses clients dont Airbus. :
Bien sûr que j'ai le compris : un tel outil doit savoir cacher ses entrailles pour exposer à l'utilisateur ses concepts métiers pour qu'il se focalise sur ce qu'il connaît. Il n'empêche que sous le capot, c'est de la traduction mathématique et de la preuve mathématique, quand bien même l'utilisateur n'en a pas conscience. Un bon outil est celui qui sait se faire discret sur son fonctionnement : celui qui l'utilise, celui qui le construit et celui qui le répare sont rarement les mêmes personnes, n'ont pas les même savoir, ni les mêmes compétences.
D'ailleurs pour illustrer la chose : je ne connaissais pas Go, si ce n'est de nom. Résultat je suis allé jeter un coup d'œil, et bien je trouve leurs choix tout sauf bêtes contrairement à ce que certains ont pu dire. Il n'y a certes pas de généricité (sauf sur quelques types comme les tuples ou les tableaux) mais leur système de type
interfaceest très ingénieux et semble compenser allègrement à l'usage l'absence de généricité. D'un point de vue formel, au premier abord (je n'ai pas creusé plus que cela) ça s'apparente grandement à des fonctions avec arguments implicites sur du lambda-calcul simplement typé avec enregistrements (un langage avec des fonctions comme citoyen de première classe pour lequel un argument de certaines fonctions est inférer par le compilateur)1 . Le polymorphisme au lieu d'être paramétrique (comme C++, Java, Haskell...) et ad-hoc mais vérifier à la compilation. Choix qui offre aux développeurs un large panel de technique de programmation sans l'assomer avec des abstractions difficiles à comprendre, donc à maîtriser et donc à utiliser (comme le sont les modules ou les GADT pour toi).Haskell a cela avec ses type classes, mais OCaml manque d'un tel dispositif ce qui rend un code qui fait un usage intensif de modules très vite incompréhensible pour celui qui n'en est pas l'auteur. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.