Encore faudrait-il être confiant dans le fait que le prouveur Coq est plus stable que la JVM...
Si stable = exempt de bugs ici, alors pour faire confiance à une preuve écrite par Coq tu dois faire confiance au coeur de Coq, relativement petit justement pour éviter les risques (+ le hardware, le compilo et autres cités plus haut mais ça s'applique aussi à la JVM).
que la probabilité d'erreur dans les preuves humaines qui se cache derrière soit plus faible que la probabilité d'erreur dans le code de la JVM.
Si la preuve passe Coq, elle est garantie sans erreur et le code généré aussi, c'est bien l'intérêt.
(bien sur en partant des principes donnés plus haut concernant le coeur de coq, le compilo, la génération de code, la théorie et autres) http://coq.inria.fr/doc/faq.html#htoc7
On tombe dans un problème d'oeuf et de poule c'est comique.
Le problème c'est qu'on ne puisse pas réécrire Coq en Coq, mais bon ! Sacré Kurt ;-)
Etant donné le nombre de personnes qui utilise Coq et le nombre de personnes qui utilisent la JVM, je suis plus que réservé...
[^] # Re: [X] : C'est exactement ce que j'espérais
Posté par lambada . En réponse au journal Sondage Java sous GPL, donnez votre avis à Sun. Évalué à 2.
Si stable = exempt de bugs ici, alors pour faire confiance à une preuve écrite par Coq tu dois faire confiance au coeur de Coq, relativement petit justement pour éviter les risques (+ le hardware, le compilo et autres cités plus haut mais ça s'applique aussi à la JVM).
Si la preuve passe Coq, elle est garantie sans erreur et le code généré aussi, c'est bien l'intérêt.
(bien sur en partant des principes donnés plus haut concernant le coeur de coq, le compilo, la génération de code, la théorie et autres)
http://coq.inria.fr/doc/faq.html#htoc7
Le problème c'est qu'on ne puisse pas réécrire Coq en Coq, mais bon ! Sacré Kurt ;-)
Etant donné le nombre de personnes qui utilise Coq et le nombre de personnes qui utilisent la JVM, je suis plus que réservé...
De toute façon j'apportais juste des précisions sur le fonctionnement de Coq, pas de son applicabilité à l'écriture d'une VM. Xavier Leroy et son équipe semblent s'intéresser à l'écriture d'un compilo prouvé formellement :
http://pauillac.inria.fr/~xleroy/compcert-backend/
http://pauillac.inria.fr/~xleroy/publi/cfront.pdf
http://groups.google.com/group/fa.caml/browse_thread/thread/(...)