a) ça fait des années que B est utilisé en milieu industriel
b) ça fait des années que Coq est «prometteur»
c) ça fait maintenant des années que METEOR tourne
La taille et la complexité ne sont pas des notions interchangeables par la seule volonté de ton intuition. Elles déterminent des domaines d'applications qui ne sont pas perméables. B a été conçu *pour* ce type de problèmes, ce n'est pas le cas pour Coq.
Ceci dit, tentons de revenir à nos moutons... ;-)
«Un gros challenge pour les méthodes formelles consiste donc certainement à un saut in the large» ...
C'est déjà le cas pour B, et peut-être même que cela pourra se faire avec des outils libres !!!
Les outils en cours de développement sont en Java mais aussi (surtout) en ... OCaml !! ;-)
Par exemple, un prouveur expérimental dénommé BPhox est en cours de réalisation. Il utilise Phox une sorte de version allégée de ... Coq !! ;-)
La boucle est bouclée. Tout le monde est content
Il y a encore beaucoup de boulot. Des volontaires ?
En particulier les outils n'ont pas d'interface ... X
:o)
[^] # Re: [HS] X, Y... Z ??? enfin B ?????
Posté par toBfree . En réponse à la dépêche Après X, voici Y.... Évalué à 0.
b) ça fait des années que Coq est «prometteur»
c) ça fait maintenant des années que METEOR tourne
La taille et la complexité ne sont pas des notions interchangeables par la seule volonté de ton intuition. Elles déterminent des domaines d'applications qui ne sont pas perméables. B a été conçu *pour* ce type de problèmes, ce n'est pas le cas pour Coq.
Ceci dit, tentons de revenir à nos moutons... ;-)
«Un gros challenge pour les méthodes formelles consiste donc certainement à un saut in the large» ...
C'est déjà le cas pour B, et peut-être même que cela pourra se faire avec des outils libres !!!
http://savannah.nongnu.org/projects/brillant/(...)
Les outils en cours de développement sont en Java mais aussi (surtout) en ... OCaml !! ;-)
Par exemple, un prouveur expérimental dénommé BPhox est en cours de réalisation. Il utilise Phox une sorte de version allégée de ... Coq !! ;-)
La boucle est bouclée. Tout le monde est content
Il y a encore beaucoup de boulot. Des volontaires ?
En particulier les outils n'ont pas d'interface ... X
:o)
Cordialement