People actually use Coq to do useful things (this is kind of harsh to Agda but whatever). Haskell isn't really the same kind of thing (I mean, ostensibly you c

People actually use Coq to do useful things (this is kind of harsh to Agda but whatever). Haskell isn't really the same kind of thing (I mean, ostensibly you could write programs in Coq, and there are some extractors to other languages, but you generally use it as a proof assistant; by contrast, writing proofs in Haskell doesn't really work unless you happen to want to prove free theorems).