Des logiques d'ordre supérieur à la programmation vérifiée en Coq

Documents et médias

Télécharger le support

pdf (2.51 Mo)

Résumé

Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d’ordre supérieur (celles où l’on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d’abord pourquoi l’ordre supérieur est plus expressif que l’ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d’axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d’axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu’on peut quantifier universellement le prédicat de travail. D’autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter.

Nous décrirons d’abord brièvement les systèmes HOL de M. Gordon, HOL-Light de J. Harrison, PVS de N. Shankar, S. Owre et J. Rushby, et Isabelle de L. Paulson, ce dernier étant en fait un méta-système logique dans lequel plusieurs logiques peuvent être définies. Ces systèmes ont conduit à des preuves très importantes en pratique : la preuve de correction de l’arithmétique entière et flottante du Pentium d’Intel par J. Harrison après le fameux bug de division du Pentium Pro qui a coûté 470 millions de dollars à Intel en 1994 ; la preuve de correction du micronoyau de système d’exploitation seL4 effectuée par G. Klein et. al. à NICTA Sydney en utilisant Isabelle (cf. le séminaire de D. Bolignano le 11 mars 2015 pour une autre preuve de système d’exploitation).

Nous présentons ensuite avec plus de détails le système Coq, développé en France et titulaire de grandes récompenses récentes. Coq est fondé sur le calcul des constructions CoC de G. Huet et T. Coquand (1984) et sa version inductive CiC développée par C. Paulin, qui parlera en séminaire, à la suite de ce cours. Coq diffère des systèmes classiques par le fait qu’il intègre complètement calcul et preuve dans un formalisme très riche, incorporant et développant considérablement des idées et théorèmes de de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc.

Gallina, le langage de programmation de Coq est un langage typé d’ordre supérieur, c’est-à-dire dont les types peuvent eux-mêmes être des fonctions. Le typage est décidable, et le système de types garantit que tous les calculs de termes bien typés se terminent sur des formes normales uniques. La programmation classique est facilitée par la couche inductive, qui permet des définitions récursives puissantes mais à terminaison garantie. Grâce à la mise en pratique de la correspondance fondamentale de Curry-Howard entre calculs et preuves, il n’y a plus vraiment de différence entre calculer et prouver. Ainsi, un programme a pour type sa spécification alors qu’une preuve a pour type le théorème qu’elle démontre, ce de façon absolument identique. De plus, les preuves sont des fonctions standards du calcul, au même titre que les fonctions sur les types de données classiques. Enfin, une fois un programme développé et prouvé en Coq, on peut en extraire automatiquement un code objet directement exécutable écrit en Caml, correct par construction et normalement efficace. Tout cela donne à Coq une richesse considérable à la fois pour spécifier, programmer, prouver et exporter, quatre activités qui deviennent complètement intégrées.

Le cours se terminera par la présentation de deux succès majeurs de Coq : d’abord le compilateur certifié CompCert de X. Leroy, seul compilateur C ayant passé le filtre des tests aléatoires présenté dans le cours du 4 mars ; ensuite la preuve complètement formelle de grands théorèmes mathématiques par G. Gonthier et. al., avec en particulier le fameux théorème de Feit-Thompson dont la preuve classique fait pas moins de 250 pages de lourdes mathématiques.