«Réelles» ça veut dire quoi? Sur des applications industrielles?
Il ne s'agit pas ici de polémiquer, mais bien de poser cette question d'un point de vue scientifique: 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, un problème d'ordonnancement (par exemple) ou un problème de maths, c'est kif-kif: c'est juste une chaîne de caractère (dotée d'une sémantique), qui est censée représenter ton problème, et sur laquelle tu effectues un certain nombre de preuves de propriétés.
L'équipe de logique de Nijmegen a ainsi formalisé et certifié en Coq le théorème de d'Alembert-Gauss, ce qui n'est pas plus simple que des problèmes industriels de petite taille.
Et c'est là qu'on peut dire par contre, qu'un problème industriel a la fâcheuse manie d'être de très grande taille, sans être forcément compliqué, d'un point de vue intuitif.
Un gros challenge pour les méthodes formelles consiste donc certainement à un saut «in the large», ce qui est très difficile pour des raisons techniques (explosion du graphe d'états). L'automatisation croissante des outils formels va dans le bon sens, mais il y a encore beaucoup de boulot.
Ce qui fait l'intérêt de la recherche: on va pas reprocher à l'équipe Coq de faire des recherches, c'est son boulot et il y a matière à recherche!
[^] # Re: [HS] X, Y... Z ??? enfin B ?????
Posté par Anaximandre . En réponse à la dépêche Après X, voici Y.... Évalué à 1.
Il ne s'agit pas ici de polémiquer, mais bien de poser cette question d'un point de vue scientifique: 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, un problème d'ordonnancement (par exemple) ou un problème de maths, c'est kif-kif: c'est juste une chaîne de caractère (dotée d'une sémantique), qui est censée représenter ton problème, et sur laquelle tu effectues un certain nombre de preuves de propriétés.
L'équipe de logique de Nijmegen a ainsi formalisé et certifié en Coq le théorème de d'Alembert-Gauss, ce qui n'est pas plus simple que des problèmes industriels de petite taille.
Et c'est là qu'on peut dire par contre, qu'un problème industriel a la fâcheuse manie d'être de très grande taille, sans être forcément compliqué, d'un point de vue intuitif.
Un gros challenge pour les méthodes formelles consiste donc certainement à un saut «in the large», ce qui est très difficile pour des raisons techniques (explosion du graphe d'états). L'automatisation croissante des outils formels va dans le bon sens, mais il y a encore beaucoup de boulot.
Ce qui fait l'intérêt de la recherche: on va pas reprocher à l'équipe Coq de faire des recherches, c'est son boulot et il y a matière à recherche!