Avec Coq, on procéde donc à la spécification du logiciel et de ses propriétés que l'on prouve dans l'assistant. Une fois que les preuves sont faite, on peux réaliser l'extraction du logiciel prouvé. Ceci est quelque chose de très nouveau et Coq est le seul logiciel le proposant pour l'instant.
Coq est généraliste mais il existe déjà des logiciels équivalents (commerciaux et non libres) dans des domaines plus spécialisés (je ne citerai que Scade+Prover).
[^] # Re: Des certifications CC-EALx
Posté par hermes42 . En réponse à la dépêche Mandrakesoft retenue pour le développement d'un système d'exploitation ouvert de haute sécurité. Évalué à 1.
Coq est généraliste mais il existe déjà des logiciels équivalents (commerciaux et non libres) dans des domaines plus spécialisés (je ne citerai que Scade+Prover).