It is more general than that: A programming language is a formal specification language that we know how to compile.

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?

▲

MaxBarraclough 4 hours ago | parent [-]

> 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...

	▲	auggierose 2 hours ago \| parent [-]
		A formal specification language doesn't have to be deterministic. And yes, if you can prove that the implementation is correct with respect to the formal spec, you are good, and it doesn't really matter how you got the implementation. Refinement is one approach, personally, I just do interactive theorem proving.