Je ne connais pas B, mais je sais qu'en Coq, tu écris ta spécification dans un langage particulier, puis la prouves interactivement, avec certaines étapes plus ou moins automatisées à l'aide de "tactiques", plusieurs bibliothèques de ces dernières étant disponibles.
Une fois la preuve établie (c'est évidemment la partie difficile), Coq est capable d'en extraire un code source en OCaml ou Haskell (via l'isomorphisme de Curry-Howard) qui sera correct par construction (si tant est que le petit coeur "trusted" de Coq, les axiomes, le compilo OCaml, le hardware, l'OS soient eux-mêmes dignes de confiance bien sur).
Coq ne part pas d'un programme pré-existant pour essayer de prouver sa correction vis à vis des spécifications.
[^] # 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é à 3.
Une fois la preuve établie (c'est évidemment la partie difficile), Coq est capable d'en extraire un code source en OCaml ou Haskell (via l'isomorphisme de Curry-Howard) qui sera correct par construction (si tant est que le petit coeur "trusted" de Coq, les axiomes, le compilo OCaml, le hardware, l'OS soient eux-mêmes dignes de confiance bien sur).
Coq ne part pas d'un programme pré-existant pour essayer de prouver sa correction vis à vis des spécifications.