Le probleme avec des programmes prouves en coq, c'est que si coq a est buggé, il peut certifier correrts des programmes buggés.
Une bonne partie de coq est elle meme prouvee a l'aide d'un noyau de coq mais de ce noyau, on sait juste qu'il est coherent, pas forcement correct.
Mais bon, quand on connait les gens qui devellopent coq (lNRIA - Logical), on peut avoir une certaine confiance dans la chose.
[^] # Re: Pas exactement
Posté par gawal . En réponse au journal La sécurité informatique au 20h de TF1. Évalué à 1.
Une bonne partie de coq est elle meme prouvee a l'aide d'un noyau de coq mais de ce noyau, on sait juste qu'il est coherent, pas forcement correct.
Mais bon, quand on connait les gens qui devellopent coq (lNRIA - Logical), on peut avoir une certaine confiance dans la chose.