Il existe un compilateur C qui est garanti "quasiment sans bug", c'est Compcert, un compilateur prouvé correct : il vient avec une preuve formelle, vérifiée par ordinateur, que si le compilateur produit un fichier assembleur alors celui-là a la même sémantique que le programme C de départ. Malheureusement, ce n'est pas du logiciel libre (restriction à un usage non-commercial), en tout cas pour l'instant.
# Compilateur sans bugs
Posté par gasche . En réponse à la dépêche OpenBSD 5.7 « Blues Brothers ». Évalué à 10.
Il existe un compilateur C qui est garanti "quasiment sans bug", c'est Compcert, un compilateur prouvé correct : il vient avec une preuve formelle, vérifiée par ordinateur, que si le compilateur produit un fichier assembleur alors celui-là a la même sémantique que le programme C de départ. Malheureusement, ce n'est pas du logiciel libre (restriction à un usage non-commercial), en tout cas pour l'instant.