Coq : un ovni fiable

Coq est un assistant de preuve français développé entre autres par l’INRIA depuis 1984.

Premièrement qu’est-ce qu’un assistant de preuve ? C’est un logiciel permettant de prouver des théorèmes ou de les formaliser. L’utilisateur doit écrire un énoncé puis fournir une preuve dont chaque étape est compréhensible par le programme. Ce dernier renvoie alors “vrai”, “faux” ou “je ne sais pas”, validant ou invalidant la preuve.

Coq permet cela et inclut en plus un langage de programmation (Gallina) ainsi que le concept d’équivalence entre une preuve et un programme.
Ainsi on peut reprendre le principe évoqué dans le paragraphe précédent :
le programmeur écrit les caractéristiques de son programme, puis écrit le code de celui ci. Coq va vérifier la validité du programme comme “preuve” des caractéristiques décrites. S’il renvoie “vrai”, c’est que le programme réalise bien la tâche demandée. Autrement dit, en théorie, un programme ne nécessite pas de débogage une fois compilé avec succès.

Une caractéristique fondamentale de Coq est qu’il n’est pas Turing complet. En d’autres termes, il ne permet pas d’effectuer toutes les tâches à la portée d’une machine de Turing. Cette caractéristique vient du fait que les fonctions récursives en Gallina doivent se terminer, acceptant en entrée uniquement des éléments de plus en plus petits.
Si par exemple on manipule une liste l, on ne peut effectuer de récursion qu’en manipulant la liste l’ qui est une sous liste de l.
Cette “limitation” est présentée comme une fonctionnalité du logiciel car elle permet de s’assurer que le programme respecte bien les spécifications entrées par le programmeur.

Enfin Coq ne supporte aucun effet de bord. Impossible donc d’écrire dans la console pour présenter un “Hello world”. Le programmeur entre du code dans Coq et celui ci l’évalue, envoyant “vrai”, “faux” ou “je ne sais pas”. Ce sont les seules interactions qui existent nativement.

Ces spécificités font de Coq un choix peu judicieux pour la plupart des applications purement informatiques. Mais dans des domaines où des bugs pourraient être catastrophiques cette manière de programmer a des adeptes. Ainsi le compilateur CompCert C a été prouvé en Coq ce qui lui permet de garantir la correspondance entre code source et code généré.