I'm not sure the comparison with Hilbert's dictum holds up in our field. Yes, Godel made a mockery of it, and mathematics is now known to be limited by incompleteness, but only at the theoretical horizon. Working mathematicians will not run into it as a problem that blocks their work in other areas.

In computing, though, the halting problem hoses us every time we have to hit ctrl-c to break an accidental infinite loop. Our tools can't always flag those situations ahead of time, so we often have to find them the hard way.

It seems clear that in software development, the specification is the program. To the extent there's something that the spec doesn't cover, that's a bug in the spec, not in the AI that turns the spec into code. Just as you wouldn't blame a compiler for your infinite loop, we will eventually reach the point where blaming a clanker for generating imperfect high-level code sounds just as bogus.

"Build me a Super Mario Bros. clone, make no mistakes" is the new hello_world.c. For anything innovative -- anything with commercial value -- the spec will have to be a lot more elaborate. There are plenty of specs that are already too complex for any one person to hold in their head, except perhaps for a few godlike prodigies. Look at the MPEG-4 document collection, or for that matter our tax and legal systems. I think the lesson is that language alone can't save us from complexity, any more than a better set of axioms can save us from incompleteness.