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.