In the general case, the "write the spec and the AI does the rest" boils down to automated theorem proving, and I'm optimistic AIs will get pretty good at this

In the general case, the "write the spec and the AI does the rest" boils down to automated theorem proving, and I'm optimistic AIs will get pretty good at this in a lot of useful situations. Even today, in limited well-defined problem spaces, there are sometimes good algorithms for this sort of thing. See Dana Angluin's algorithm for learning the DFA that recognizes a regular language given through an interactive process of having the user provide examples/counterexamples, which serve to provide an increasingly constrained spec.