Sur le fond je pense que nous sommes plutôt d'accord. Voici quand même quelques remarques.
a) ça fait des années que B est utilisé en milieu industriel
c) ça fait maintenant des années que METEOR tourne
N'en rajoute pas tout de même, ce n'est pas encore la consécration. Il y a eu un développement marquant (le système de freinage de METEOR) mais pas grand-chose depuis.
b) ça fait des années que Coq est «prometteur»
Rappelons tout de même que la théorie axiomatique des ensembles date de 1910-1920 alors que la théorie des types a réellement débuté en 1971 (Martin-Löf). Il reste beaucoup de choses à construire, d'autant plus que la théorie des types est plus complexe que la théorie des ensembles (notamment à cause du manque d'extensionnalité).
J'ajoute que B est lui aussi encore en développement: B événementiel, mais aussi définitions inductives (un des derniers dadas d'Abrial) de structures complexes (au lieu d'en rester à certains types de données prédéfinis), etc.
La taille et la complexité ne sont pas des notions interchangeables par la seule volonté de ton intuition.
Je ne crois pas avoir écrit cela mais : «y a-t-il une différence réelle entre un problème industriel et un problème mathématique, du point de vue de la difficulté intellectuelle de la tâche? Je n'en suis pas sûr.» D'un point de vue formel, spécifier un problème de maths ou plus orienté systèmes, c'est pas vraiment différent.
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.
Effectivement, B est orienté systèmes, surtout avec son procédé de raffinement jusqu'au B0. Et Coq est généraliste dans l'absolu, même si les développements marquants sont en maths formelles. On a quand même les types coïnductifs et l'extraction de code, de même que l'annotation de programmes impératifs (à la Floyd-Hoare et... B).
C'est déjà le cas pour B
Là je ne suis pas d'accord: même pour B ce n'est pas le cas. Le système de freinage de METEOR fait environ 60.000 lignes d'Ada (Abrial dixit) si mes souvenirs sont bons. On est loin d'un programme industriel de plusieurs millions de lignes.
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
C'est rigolo mais parmi les participants, je connais un chargé de recherche (collègue de bureau) qui utilisait Coq pour prouver du B parce que l'Atelier B n'est pas assez puissant!
Quant à PhoX, ce n'est pas un Coq light. C'est un assistant fondé sur la logique classique d'ordre supérieur (implémentée en AF2), pas du tout sur le calcul des constructions inductives, qui est en plus intuitionniste. Cela dit, PhoX est vraiment très agréable à utiliser et très «pragmatique».
[^] # Re: [HS] X, Y... Z ??? enfin B ?????
Posté par Anaximandre . En réponse à la dépêche Après X, voici Y.... Évalué à 0.
a) ça fait des années que B est utilisé en milieu industriel
c) ça fait maintenant des années que METEOR tourne
N'en rajoute pas tout de même, ce n'est pas encore la consécration. Il y a eu un développement marquant (le système de freinage de METEOR) mais pas grand-chose depuis.
b) ça fait des années que Coq est «prometteur»
Rappelons tout de même que la théorie axiomatique des ensembles date de 1910-1920 alors que la théorie des types a réellement débuté en 1971 (Martin-Löf). Il reste beaucoup de choses à construire, d'autant plus que la théorie des types est plus complexe que la théorie des ensembles (notamment à cause du manque d'extensionnalité).
J'ajoute que B est lui aussi encore en développement: B événementiel, mais aussi définitions inductives (un des derniers dadas d'Abrial) de structures complexes (au lieu d'en rester à certains types de données prédéfinis), etc.
La taille et la complexité ne sont pas des notions interchangeables par la seule volonté de ton intuition.
Je ne crois pas avoir écrit cela mais : «y a-t-il une différence réelle entre un problème industriel et un problème mathématique, du point de vue de la difficulté intellectuelle de la tâche? Je n'en suis pas sûr.» D'un point de vue formel, spécifier un problème de maths ou plus orienté systèmes, c'est pas vraiment différent.
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.
Effectivement, B est orienté systèmes, surtout avec son procédé de raffinement jusqu'au B0. Et Coq est généraliste dans l'absolu, même si les développements marquants sont en maths formelles. On a quand même les types coïnductifs et l'extraction de code, de même que l'annotation de programmes impératifs (à la Floyd-Hoare et... B).
C'est déjà le cas pour B
Là je ne suis pas d'accord: même pour B ce n'est pas le cas. Le système de freinage de METEOR fait environ 60.000 lignes d'Ada (Abrial dixit) si mes souvenirs sont bons. On est loin d'un programme industriel de plusieurs millions de lignes.
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
C'est rigolo mais parmi les participants, je connais un chargé de recherche (collègue de bureau) qui utilisait Coq pour prouver du B parce que l'Atelier B n'est pas assez puissant!
Quant à PhoX, ce n'est pas un Coq light. C'est un assistant fondé sur la logique classique d'ordre supérieur (implémentée en AF2), pas du tout sur le calcul des constructions inductives, qui est en plus intuitionniste. Cela dit, PhoX est vraiment très agréable à utiliser et très «pragmatique».