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 :)
# 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 :)