Coq permet de montrer des choses, par exemple qu'un programme a le comportement voulu. Un exemple célèbre est celui de la ligne de Métro 14 à Paris, dont le système automatique aurait été montré sans bug :)
Il y a une interface pour emacs
Il est utilisé en module de Programmation Fonctionnelle et Preuve
8.0beta