Well, I'd claim that Idris is pretty much that. A general purpose (if highly experimental) programming language with the power of a proof assistant. Also, I ha

Well, I'd claim that Idris is pretty much that. A general purpose (if highly experimental) programming language with the power of a proof assistant. Also, I have seen people write proofs in Coq and extract them to compilable OCaml source code.