The question of how to make good use of AI in software development has been open for almost forty years at least -- ever since Rich and Waters' Programmer's Apprentice project [1] produced rather unexciting results. (I don't recall in detail what they did, but it didn't set the world on fire.) The failure of Prolog -- not that it failed to be useful at all, but it failed to live up to the hopes -- is instructive. Prolog never delivered on the promise of declarative programming, because its rigid, unintelligent depth-first search strategy makes it necessary to understand the execution model and keep it in mind when writing programs. So it's only mostly declarative. Prolog achieved some popularity because there are times when brute-force depth-first search is all you need, particularly if it can be done very fast; but once you bump against the limitations of that paradigm, Prolog is of little help.
I think this failure is instructive. The key problem, I believe, is controlling search. Search is necessary for reasoning about programs; this is a consequence of Turing's famous Halting Problem proof. But searching -- particularly, searching the massive spaces of possible programs and of possible invariants of programs -- without getting lost is very difficult.
You can't understand a program without understanding its invariants. All interesting programs contain recursion (iteration being a special case of recursion), and understanding a recursive program requires knowing the postcondition of the recursion. That in turn requires coming up with the correct induction hypothesis. A simple example to clarify the meaning of the terms:
int a[5];
for (int i = 0; i < 5; i++) a[i] = 42;
The postcondition of this loop is:
∀i 0 ≤ i < 5 ⇒ a[i] = 42
which says that all 5 elements of the array are equal to 42. The induction hypothesis is:
where a' is the value of a at the bottom of the loop; this says that if all the elements of a below i are 42 at the top of the loop, then all the elements through i (note the "j ≤ i") are 42 at the bottom. Once we have this induction hypothesis, it's trivial to prove it, and once we've proven it, it's trivial to prove the postcondition. In simple cases like this, human programmers do all this reasoning subconsciously; it's second nature to us. Not so easy for machines, though.
The problem in a nutshell is that search is required to find the induction hypothesis; there's no algorithm that will produce it. (This is a clear consequence of the Halting Problem.) While it seems straightforward in this case, we all know that most programs aren't anywhere near this simple. And the search required for real-world cases is still beyond existing AI technology.
Seeing your example does make me wonder if the an AI of that level is truly out of reach. It's well known that human reasoning is flawed by cheap heuristics thrown in by nature and/or selection.
Looking at your examples you'd think that just throwing enough memory/speed/power at a simple bruteforce/search approach would solve trivial examples.
Not to mention that when a programmer analyses code he's actually executing it inside his head. Perhaps not all the loops, but looking at a loop he will follow the steps in the code. So in a sense he is executing a piece of code inside his head, thus not violating and/or disproving the halting problem(?).
While precondition generation is indeed a very hard problem, for programs such as your example we actually have methods that work. See for example these for sets of slides and the references therein
What do you think about the newer attempts at declarative programming (which are often embedded in Prolog) such as CLP + consistency techniques and CHR?
Regardless of whether Prolog (or CLP or CHR) is helpful towards "real" AI, I'd like to hear your thoughts about the kind of domains / problems for which these approaches are a good fit.
Prolog is not AI, as the Japanese discovered [0].
The question of how to make good use of AI in software development has been open for almost forty years at least -- ever since Rich and Waters' Programmer's Apprentice project [1] produced rather unexciting results. (I don't recall in detail what they did, but it didn't set the world on fire.) The failure of Prolog -- not that it failed to be useful at all, but it failed to live up to the hopes -- is instructive. Prolog never delivered on the promise of declarative programming, because its rigid, unintelligent depth-first search strategy makes it necessary to understand the execution model and keep it in mind when writing programs. So it's only mostly declarative. Prolog achieved some popularity because there are times when brute-force depth-first search is all you need, particularly if it can be done very fast; but once you bump against the limitations of that paradigm, Prolog is of little help.
I think this failure is instructive. The key problem, I believe, is controlling search. Search is necessary for reasoning about programs; this is a consequence of Turing's famous Halting Problem proof. But searching -- particularly, searching the massive spaces of possible programs and of possible invariants of programs -- without getting lost is very difficult.
You can't understand a program without understanding its invariants. All interesting programs contain recursion (iteration being a special case of recursion), and understanding a recursive program requires knowing the postcondition of the recursion. That in turn requires coming up with the correct induction hypothesis. A simple example to clarify the meaning of the terms:
The postcondition of this loop is: which says that all 5 elements of the array are equal to 42. The induction hypothesis is: where a' is the value of a at the bottom of the loop; this says that if all the elements of a below i are 42 at the top of the loop, then all the elements through i (note the "j ≤ i") are 42 at the bottom. Once we have this induction hypothesis, it's trivial to prove it, and once we've proven it, it's trivial to prove the postcondition. In simple cases like this, human programmers do all this reasoning subconsciously; it's second nature to us. Not so easy for machines, though.The problem in a nutshell is that search is required to find the induction hypothesis; there's no algorithm that will produce it. (This is a clear consequence of the Halting Problem.) While it seems straightforward in this case, we all know that most programs aren't anywhere near this simple. And the search required for real-world cases is still beyond existing AI technology.
[0] http://en.wikipedia.org/wiki/Fifth_generation_computer [1] http://dspace.mit.edu/handle/1721.1/6054