Posté par anaseto .
En réponse au journal C++17 est sur les rails.
Évalué à 3.
Dernière modification le 22 mars 2016 à 08:51.
un programme Coq qui compile est garanti sans bug
Encore faut-il que les propriétés écrites qui sont prouvées soient les bonnes :) Donc dans le cas d'un compilo, principalement que la sémantique du langage initial soit écrite correctement (les rares bugs trouvés l'ont été à ce niveau pour CompCert). Ceci dit, un programme Coq qui compile, même sans preuves, apporte au moins la terminaison.
comme le compilateur CompCert (le seul à ma connaissance)
Le seul (que je sache) qui ait une chaîne complète (à quelques petits bouts près au début et à la fin), oui. Sinon il y a aussi eu quelques efforts pour formaliser l'IR de LLVM et quelques optims, par exemple.
[^] # Re: C'est bien dommage
Posté par anaseto . En réponse au journal C++17 est sur les rails. Évalué à 3. Dernière modification le 22 mars 2016 à 08:51.
Encore faut-il que les propriétés écrites qui sont prouvées soient les bonnes :) Donc dans le cas d'un compilo, principalement que la sémantique du langage initial soit écrite correctement (les rares bugs trouvés l'ont été à ce niveau pour CompCert). Ceci dit, un programme Coq qui compile, même sans preuves, apporte au moins la terminaison.
Le seul (que je sache) qui ait une chaîne complète (à quelques petits bouts près au début et à la fin), oui. Sinon il y a aussi eu quelques efforts pour formaliser l'IR de LLVM et quelques optims, par exemple.