Comment by tossandthrow

A compiler does not transalte specs to code.

Specs are denotational by nature.

A program could synthesize a program that adheres to the specs. But that is not what we understand by a compiler that generally has to preserve operational semantics.