The problems the OP wants to solve are formally undecidable and reducible to the halting problem.
While this is true in general, our current "solution" to the problem - hire a human programmer, give him the spec, and set him loose - doesn't do any better here. The problems we as an entire field "want to solve" are, in general, formally undecidable and reducible to the halting problem, but we get by anyways because it turns out that you can get a lot of useful work done even without solving the general problem.
I see no reason that a well-designed system couldn't similarly leverage "special cases" that are not undecidable. How efficiently this could be done is another matter, but I think step one in that direction is to accept a pretty major loss of generality - after all, that's how humans get the job done, and for the most part we're still able to turn most of the specs that we're faced with into working code, given enough time.
While this is true in general, our current "solution" to the problem - hire a human programmer, give him the spec, and set him loose - doesn't do any better here. The problems we as an entire field "want to solve" are, in general, formally undecidable and reducible to the halting problem, but we get by anyways because it turns out that you can get a lot of useful work done even without solving the general problem.
I see no reason that a well-designed system couldn't similarly leverage "special cases" that are not undecidable. How efficiently this could be done is another matter, but I think step one in that direction is to accept a pretty major loss of generality - after all, that's how humans get the job done, and for the most part we're still able to turn most of the specs that we're faced with into working code, given enough time.