[sakoht]

"Wouldn't it just be grand if we could write a spec for some piece of code, then let the machines do the rest?"

This is quite possible, if you write the "spec" in a programming language: i.e. write a test case. The problem is that people imagine a formal proof in, for example, English, being simpler or easier to think about than in, say, Python or C. In general this is not true. In general, moment you expect your "spec" (code) to be sufficiently precise for a machine to act upon it, the simplest way to describe it is a programming language.

And if you can invent a better way to describe it, and it is unambiguous enough for a machine to act on it, you've invented a new programming language.