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

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.