GitHub - tcarstens/verlangCoq is an environment for functional programming with an integrated proof agent. The software development process with Coq is a bit non-standard: one doesn't ordinarily compile Coq source directly, but instead "extracts" the computationally-relevant portions to another language. Coq supports extraction to OCaml, Haskell, and Scheme, though at time of writing the OCaml target is the most mature. Er
