Coq est un assistant de preuve utilisant le langage Gallina, développé par l’Institut de recherche en informatique fondamentale (une unité mixte entre le CNRS et l’Université de Paris hébergeant une équipe de l’INRIA), en partenariat avec l’École polytechnique et le CNAM.
Un assistant de preuve est un logiciel qui permet d’écrire et de vérifier des preuves mathématiques, soit sur des théorèmes, soit sur des assertions relatives à l’exécution de programmes informatiques.
À l’origine, il fut appelé CoC, une abréviation en anglais de « calcul des constructions » sur lequel il est fondé. Le calcul des constructions fut introduit par Thierry Coquand.
La métaphore avec le symbole de la France est filée : son langage est Gallina et son wiki s’appelle Cocorico !
Coq a été récompensé par le prix 2013 des langages de programmation de l’ACM.
Malheureusement, Coq va être renommé, parce qu’il se prononce de la même manière que cock en anglais, qui est l’argot pour « bite, pénis », ce que la plupart des personnes parlant anglais trouvent repoussant.
Comme Coq est un logiciel libre, son nom ne doit pas faire obstacle au recrutement de contributeurs, en particulier les femmes.
Un appel est donc lancé sur le site GitHub de l’assistant de preuve, pour trouver un nouveau nom.