3 ms·
Coq is a theorem prover and library that is written in ML (OCaml), so it is definitely not Haskell. It is interesting that most (interactive) proof systems (e.
by protomikron 10y ago
Coq is a theorem prover and library that is written in ML (OCaml), so it is definitely not Haskell.
It is interesting that most (interactive) proof systems (e.g. Isabelle and Coq) are written in ML, I think it is probably historical. AFAIK most theorem proving research is done in Europe and ML has always been more popular there (however it seems to change in recent years, and FP courses switch to Haskell - however my school e.g. switched from OCaml to Haskell to OCaml in their FP course).
- 0xmohit 10y agoOP said: > My biggest problem with pure FP languages is a lack of interesting projects The list included projected written in pure FP languages. Not only COQ, Flow is also written in OCaml.
- protomikron 10y agoYou are right my mistake. However it seems to me that the Haskell community lays more emphasis on purity and the OCaml community takes a more pragmatic approach - but this distinction may be superficial for practical concerns.