I'm afraid I don't know enough about dependent types and PL theory to really explain this well, but bear in mind that you're on page 35. You can use program ext

I'm afraid I don't know enough about dependent types and PL theory to really explain this well, but bear in mind that you're on page 35. You can use program extraction on a proof itself and yield an executable program. You can use program extraction on anything in Coq, so if you use it as an implementation language you can compile it down to OCaml (or Rust now!) after proving your implementation correct. I suppose it's possible that there are only some programs and proofs amenable to being written that way, but also suspect that's more due to the human difficulty than anything else.