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

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 https://en.wikipedia.org/wiki/AKS_primality_test