Bonjour

Depuis quelques jours, je découvre une famille de logiciels amusants qui s'appellent les "assistants de preuves", comme Coq ou Isabelle. Ce sont des logiciels apparemment peu connus (même si je sais que certains Zéros ici en ont déjà utilisé) mais qui permettent d'aider un mathématicien ou un informaticien à rédiger une preuve mathématique : ils indiquent les buts et les sous-buts, permettent de réécrire automatiquement certaines expressions, et surtout ils empêchent de croire que l'on a démontré quelque chose alors qu'en réalité non. La contrepartie est qu'ils imposent un formalisme qui peut être un peu lourd pour des problèmes avancés.

Les assistants de preuves ont une utilité réelle : par exemple Isabelle a servi à formaliser et à vérifier le code du noyau L4, ce qui a permis de détecter des bugs. Je crois que les développeurs de Coq, l'INRIA, ont fait la même chose sur un compilateur C. Apparemment, Isabelle est basé sur des assistants plus anciens, et a donc eu le temps de mieux s'installer (notamment dans l'industrie). Cependant je trouve Coq plus intuitif, et surtout il y a plus de documentation en français, ce qui peut être un avantage pour certains ! Vous trouverez des exemples ici

J'ai quelques questions : j'aimerais savoir si quelqu'un connaît mieux les différences entre les deux assistants. Je sais qu'ils n'ont pas les mêmes fondements théoriques, mais est-ce que ça a une importance en pratique ? Est-ce qu'il y en a un qui est fondamentalement plus puissant que l'autre, ou qui pourrait être plus facile à utiliser pour certains domaines ? Apparemment, Isabelle est basé sur de la simple réécriture (acceptant plusieurs systèmes logiques) alors que Coq est basé sur le Calcul des Constructions, qui est un cas particulier de logique d'ordre supérieur...

Et, surtout, est-ce que ça vous intéresse ou bien il n'y a que moi ?

Citation : Litewolf

Je sais qu'ils n'ont pas les mêmes fondements théoriques, mais est-ce que ça a une importance en pratique ? Est-ce qu'il y en a un qui est fondamentalement plus puissant que l'autre, ou qui pourrait être plus facile à utiliser pour certains domaines ? Apparemment, Isabelle est basé sur de la simple réécriture (acceptant plusieurs systèmes logiques) alors que Coq est basé sur le Calcul des Constructions, qui est un cas particulier de logique d'ordre supérieur...

Je pense que ta question (qu'on pourrait résumer à « quel assistant de preuve utiliser ? ») est traitée partiellement par Adam Chlipala dans son livre Certified Programming with Dependent Types. Il y explique en effet pourquoi il a choisi d'utiliser Coq et pas un autre langage à la mode (comme Agda), et ça pourrait t'intéresser.

Sinon oui, il y'a quelques autres personnes qui s'intéressent aux assistants de preuve par ici même si ils ne sont pas très bruyants (il y'en a d'ailleurs un qui a écrit une série d'articles d'introduction à Coq). Si tu as une questions nous pourrons toutefois probablement essayer de t'aider (pour Coq du moins).

Bonne soirée.

J'ai déjà commencé ce livre, et effectivement Adam Chlipala compare un petit peu les différents assistants de preuve. Il semble dire que certains utilisant les types dépendants sont moins puissants que Coq, car plus restreints. Mais il ne compare pas vraiment l'ensemble de ce qui est possible avec Isabelle/HOL et Coq, il dit juste que Coq est plus expressif grâce aux types dépendants...

Apparemment tu connais déjà un peu Coq, tu l'as déjà utilisé pourquoi faire ? Je vais lire les articles que tu parles. Ils n'ont pas l'air d'aller très loin.