A formal specification language is a programming language that we don't know how to compile.

If we can use AI to automatically implement a formal spec, then that formal specification language has just become a programming language.

▲

MaxBarraclough 4 hours ago | parent | next [-]

> A formal specification language is a programming language that we don't know how to compile.

Not really, on both counts.

Firstly they're not really programming languages in the usual sense, in that they don't describe the sequence of instructions that the computer must follow. Functional programming languages are considered 'declarative', but they're still explicit about the computational work to be done. A formal spec doesn't do this, it just expresses the intended constraints on the correspondence between input and output (very roughly speaking).

Secondly, regarding the we don't know how to compile it aspect: 'constraint programming' and SMT solvers essentially do this, although they're not a practical way to build most software.

▲

auggierose 6 hours ago | parent | prev | next [-]

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.

▲

pron an hour ago | parent | prev [-]

Except deciding whether an implementation exists or not is itself not a tractable problem in the general case.