Apprendre Coq
Coq, assistant de preuve

Face à l’importance croissante des composants informatiques – logiciels et matériels – dans des domaines critiques aussi divers que transports, énergie, santé, finance, etc., le besoin de composants sûrs se fait de plus en plus impérieux.

Par exemple, l’exécution d’un programme doit se faire sans erreur dans les conditions d’application prévues : absence d’erreur à l’exécution ou de bouclage non désiré, conformité à une spécification fonctionnelle.

Or nous savons, depuis Turing , qu’aucun algorithme ne peut automatiquement prendre en donnée un programme quelconque et rendre en un temps fini un diagnostic de correction. Par conséquent, seule une partie de la tâche de certification d’un logiciel peut être automatisée. Pour le reste, on peut recourir à des outils interactifs, où la preuve – souvent complexe – de correction doit être guidée par l’utilisateur.

Les assistants de preuve sont des logiciels interactifs permettant à leur utilisateur de prouver des théorèmes en le déchargeant des tâches fastidieuses et susceptibles d’être entachées d’erreurs. Outre cette fonction d’assistance à l’écriture de démonstrations, ces logiciels vérifient que toutes les preuves construites sont complètes et respectent toutes les lois de la logique.

Par « théorème », nous entendons toute sorte d’énoncé concernant soit le domaine mathématique, soit le comportement de programmes écrits dans un langage donné. Citons deux exemples, prouvés en Coq :

« Toute carte planaire peut être coloriée avec au plus quatre couleurs. »

Le compilateur CompCert garantit que tout code exécutable qu’il génère se comporte exactement comme le programme source C dont il est issu .

Coq est un logiciel puissant et complexe, en constante évolution. Dans cet article, nous proposons en première partie une introduction sur un exemple très simple de preuve d’un petit programme fonctionnel. Une deuxième partie présente quelques applications de taille réelle. Nous terminerons par des indications sur l’apprentissage de Coq et des précisions sur l’évolution de cet outil.