The Coq mailing list

[AUGER Cedric <sedrikov AT gmail.com>]

nana nana wrote:
> Bonjour,
> je travail sur la verification de code pour les systemes embarqu=E9s et je
> trouve Coq .
> j'ai une question svp :
> est ce que Coq peut verifier un code ecrit dans autre langage ou bien en
> l'utilise pour realiser un verifieur ?
> c tres urgent pour moi,
> j'atends votre reponse.
> merci
>
>  
Bonjour,
je ne suis pas sûr que tu aies besoin de Coq pour ça, je n'ai jamais 
utilisé d'autre logiciel de ce type, jete un oeil à:
http://pvs.csl.sri.com
http://www.cs.utexas.edu/~moore/acl2
http://why.lri.fr/index.fr.html

Coq n'est pas à proprement parler un vérificateur de programme, (enfin 
ça dépend de quel côté de l'isomorphisme de Curry-Howard tu te places).
En fait c'est un assistant de preuve, c'est à dire que tu dois fabriquer 
toi même une preuve, et Coq te répond si il a trouvé une erreur dans ta 
preuve.

Enfin si tu veux davantage de réponses, tape un message en anglais, 
c'est ce qu'on fait tous ici (même si très souvent ce sont des français 
qui répondent à des français), ou au moins en bon français, (pas de 
style SMS), et relis toi... (Je ne suis pas sur d'avoir compris ta 
question par exemple, principalement du fait de quelques erreurs de 
syntaxe).