Coq offre tout à la fois un langage de programmation fonctionnelle à types dépendants et un formalisme logique qui, ensemble, permettent tout autant le développement de théories mathématiques que la spécification et la certification de propriétés de programmes. Coq fournit aussi un ensemble vaste et extensible de méthodes de preuve. Les programmes de Coq sont extractibles vers OCaml, Haskell, Scheme...
