Ahem, comparer coq à SCADE n'est pas vraiment adapté.
PROVER, c'est un prouver automatique (c'est un moteur SAT). Le langage sous-jascent est donc forcément moins expressif. Coq, c'est tout le contraire: C'est un langage très puissant (logique d'ordre supérieur, un truc qui ressemble à CAML), mais il faut *tout* prouver à la main. En général, le premier exercice qu'on donne à un débutant en coq, c'est de prouver que 1 != 0, et il faut déjà un certain temps pour y arriver. A ma connaissance, le plus gros programme jamais prouvé en coq fait 20 000 lignes.
Enfin, en tous cas, si tu vas dire aux gens qui font SCADE (ou la version académique, Lustre) que c'est "équivalent" à coq, tu risques ne ne pas en ressortir vivant, et réciproquement ;-)
[^] # Re: Des certifications CC-EALx
Posté par Matthieu Moy (site web personnel) . 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é à 3.
PROVER, c'est un prouver automatique (c'est un moteur SAT). Le langage sous-jascent est donc forcément moins expressif. Coq, c'est tout le contraire: C'est un langage très puissant (logique d'ordre supérieur, un truc qui ressemble à CAML), mais il faut *tout* prouver à la main. En général, le premier exercice qu'on donne à un débutant en coq, c'est de prouver que 1 != 0, et il faut déjà un certain temps pour y arriver. A ma connaissance, le plus gros programme jamais prouvé en coq fait 20 000 lignes.
Enfin, en tous cas, si tu vas dire aux gens qui font SCADE (ou la version académique, Lustre) que c'est "équivalent" à coq, tu risques ne ne pas en ressortir vivant, et réciproquement ;-)