You've just invented the field of program synthesis, which is a super active research area right now in programming languages! Here's the paper list from a class at UW focused on this area: http://courses.cs.washington.edu/courses/cse599a2/15wi/ . The Sumit Gulwani paper from the first week is a really good introduction to the field.

Aside from program synthesis, there is the more restricted form of code extraction, which turns definitions inside a theorem prover into code in a more traditional, runnable language such as OCaml. But you'll still want to do one or more refinement steps inside the theorem prover where you turn your spec into more efficient definitions (or even definitions that are computable at all - how do you evaluate an unbounded universal quantifier?)

As others have already replied, sometimes it can. But sometimes, and particularly if we care about efficiency, this is so difficult that we're not even close to being able to automate it.

For example, here is my "formal definition" of a primality checker:

IsPrime(Int n) = n > 1 and not(exists a, b in Int: a > 1 and b > 1 and a * b == n)

It is not directly executable, because it uses the "exists" quantifier over all integers. A clever code extractor should be able to somehow convert this to a finite computation. But would it be able to come up with the polynomial-time AKS primality test? [1] I highly doubt it.

Unless, of course, there is a special case for recognizing this particular definition. But I don't think that really counts, because I'm only using primality checking as an example. You can't have a special case for everything.

[1] https://en.wikipedia.org/wiki/AKS_primality_test

Well then the spec isn't just a spec. It is a programming language in and of itself.

And how do you prove that THAT spec is correct?

It is turtle specs all the way down.

Have a look at Why3 for example or Coq. That's exactly what formal verification systems do: 1. Formally prove intention. 2. Generate code.