> A programming language is a formal specification language that we know how to compile

Plenty of real programming languages are ambiguous in ways that surely disqualify them as formal specification languages. A trivial example in C: decrementing an unsigned int variable that holds 0. The subtraction is guaranteed to wrap around, but the value you get depends on the platform, per the C standard.

> There are plenty of formal specifications that cannot be compiled, even not by an AI. If you use AI, how do you make sure that the AI compiler compiles correctly?

By proving that the code satisfies the formal spec. Getting from a formal spec to a program (in an imperative programming language, say) can be broken down into several stages of 'refinement'. A snippet from [0] :

> properties that are proved at the abstract level are maintained through refinement, hence are guaranteed to be satisfied also by later refinements.

[0] https://www.southampton.ac.uk/~tsh2n14/publications/chapters...