If you're interested in this kind of thing, note that Coq can also extract code in Haskell, Scheme and OCaml.
If Coq's not quite your cup of tea, Isabelle/HOL is another proof assistant with amazing (dare I say superior?) tooling and automation, and it supports code extraction in SML, OCaml, Haskell and Scala.
Microsoft Research's Lean theorem prover is also promising in this regard. Work is almost complete on native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code. (see https://github.com/leanprover/lean/pull/1241 for progress)
(Note that none of those code extractors are verified to be correct themselves, lacking a formalization of the target language's semantics. You don't get a mathematical proof that the code you're running does what you specified, but you get pretty damn close.)
>Note that none of those code extractors are verified to be
>correct themselves, lacking a formalization of the target
>language's semantics.
CertiCoq project aims to provide a certified compiler from Coq into CLight (formalized subset of "Safe C"). In this respect,
it is superior to what you have mentioned, I guess.
Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous,
I feel doubt in its reliability.
https://www.cl.cam.ac.uk/~mom22/
This data structure refinement with one version getting automated to a large degree:
https://www21.in.tum.de/~lammich/pub/cpp2016_impds.pdf
Thanks to DeepSpec, Coq might exceed that in some ways:
Note that a lot of work around Coq goes through CompCert which is proprietary software with restrictions on how it's used if one doesn't pay. The Isabelle/HOL alternatives like Simpl/C and CakeML are free software. Then, outside those two, we got a bunch of work being done in Maude (esp K Framework) with one an executable, formal semantics for C done like a compiler: