Coq is first and foremost a proof assistant, you can construct theorems in types and inhabitants of those types constitute proofs of theorems. it's based on a m

Coq is first and foremost a proof assistant, you can construct theorems in types and inhabitants of those types constitute proofs of theorems. it's based on a much more advanced type system called the Calculus of Constructions[1]. Coq is not suited for writing programs, though some people do use it to extract formally verified code in some highly specialized cases. Haskell is a general purpose high-level language suitable for writing any kind of high-level program. [1] http://en.wikipedia.org/wiki/Calculus_of_constructions http://en.wikipedia.org/wiki/Calculus_of_constructions