Coq doesn't really provide a suitable environment for executing real software AFAIK; it's designed so that, once you've proven your code correct, it can extract

Coq doesn't really provide a suitable environment for executing real software AFAIK; it's designed so that, once you've proven your code correct, it can extract a Haskell or Ocaml program out of it.