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.
Effectivement, mais cela a été corrigé. Je ne suis pas rentré dans les détails dans le journal, mais Gérard Berry en parle dans sa présentation dont le lien est dans le journal (il y parle aussi du projet deepspec) :
L’importance de CompCert devient claire quand on regarde d’autres projets comme l’outil Csmith développé à l’université d’Utah, qui, à l’aide de techniques de génération aléatoire, a permis d’engendrer automatiquement un million de programmes C destinés à casser les compilateurs. Le résultat a été étonnant : Csmith a permis de détecter des centaines de bugs dans les principaux compilateurs C, mais aucun dans CompCert (en fait deux au début, mais pas dans les parties bien définies de C, et ces bugs ont ensuite été corrigés).
En ce qui concerne les approches formelles :
On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité.
Cette remarque s'applique inéluctablement à la conception de matériel qui repose sur des théories physiques qui sont une modélisation de la réalité. Comment prouver que le modèle « correspond » au réel ? Et d'ailleurs quel sens pourrait bien avoir une telle question ?
Pour ce qui est de la formalisation de processus de calcul, ce n'est pas le cas. Mais on peut tomber sur d'autres problématiques ironiquement bien formulées dans cet article :
1973 - Robin Milner creates ML, a language based on the M&M type theory. ML begets SML which has a formally specified semantics. When asked for a formal semantics of the formal semantics Milner's head explodes.
Robin Milner est un des pères fondateurs de la discipline dans laquelle travaille Xavier Leroy : la preuve mathématique assistée par ordinateur. Le langage OCaml est un langage de la famille ML, et tous les langages de cette famille (avec SML, OCaml, Haskell, Coq, Idris...) sont tous fondés sur la correspondance de Curry-Howard ou correspondance preuve-programme : un programme est une preuve d'un théorème mathématique et son type est l'énoncé du théorème.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Nuance
Posté par kantien . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 5.
Effectivement, mais cela a été corrigé. Je ne suis pas rentré dans les détails dans le journal, mais Gérard Berry en parle dans sa présentation dont le lien est dans le journal (il y parle aussi du projet deepspec) :
En ce qui concerne les approches formelles :
Cette remarque s'applique inéluctablement à la conception de matériel qui repose sur des théories physiques qui sont une modélisation de la réalité. Comment prouver que le modèle « correspond » au réel ? Et d'ailleurs quel sens pourrait bien avoir une telle question ?
Pour ce qui est de la formalisation de processus de calcul, ce n'est pas le cas. Mais on peut tomber sur d'autres problématiques ironiquement bien formulées dans cet article :
Robin Milner est un des pères fondateurs de la discipline dans laquelle travaille Xavier Leroy : la preuve mathématique assistée par ordinateur. Le langage OCaml est un langage de la famille ML, et tous les langages de cette famille (avec SML, OCaml, Haskell, Coq, Idris...) sont tous fondés sur la correspondance de Curry-Howard ou correspondance preuve-programme : un programme est une preuve d'un théorème mathématique et son type est l'énoncé du théorème.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.