Il serait donc peut être intéressant qu'un jour, une équipe, comme celle de Xavier Leroy à l'INRIA s'amuse à prouver quelques morceaux du compilateur.
Ce qui a été fait pour un compîlateur mini C.
Et la marmotte qui met le chocolat dans le papier d'alu, tu la prouves aussi en Coq ?
Sérieusement, on est très très très très loin de pouvoir prouver du code C un tant soit peu non trivial, alors des bouts de gcc...
[^] # Re: Esperons que la qualité suivra
Posté par Zakath . En réponse à la dépêche Sortie de la version 4.1 du compilateur GCC. Évalué à -1.
Et la marmotte qui met le chocolat dans le papier d'alu, tu la prouves aussi en Coq ?
Sérieusement, on est très très très très loin de pouvoir prouver du code C un tant soit peu non trivial, alors des bouts de gcc...