Posté par Lucas .
En réponse à la dépêche [code] Trouver les erreurs.
Évalué à 4.
Dernière modification le 26 janvier 2015 à 18:22.
Bien sûr il est irréaliste de vouloir développer un programme d'envergure en Coq mais ces techniques commence à être disponibles sur des langages "mainstream".
Laborieux, certes, irréaliste pas sûr... Connais tu compcert ?
C'est un compilateur C écrit en Coq dont chaque représentation interne est formellement spécifiée et chaque transformation est formellement prouvée en Coq (notamment les optimisations qu'il applique).
[^] # Re: Une autre approche est possible
Posté par Lucas . En réponse à la dépêche [code] Trouver les erreurs. Évalué à 4. Dernière modification le 26 janvier 2015 à 18:22.
Laborieux, certes, irréaliste pas sûr... Connais tu compcert ?
C'est un compilateur C écrit en Coq dont chaque représentation interne est formellement spécifiée et chaque transformation est formellement prouvée en Coq (notamment les optimisations qu'il applique).
edit : je voulais répondre à newca, pardon...