> The synthesis algorithm takes a generate-and-test approach: it generates an infinite stream of all the expressions having the same type as f; then, they are tested against the given predicate.
I'm really impressed that such a simple approach works. Initially I thought it was something similar to FOIL[0]. FOIL was a program that could learn function definitions by examples. One version of FOIL was able to solve exercises from a Prolog book. For one of the exercises, it was able to come up with a solution that was shorter than what humans had previously come up with. I don't remember exactly how FOIL worked, but if I recall correctly, it would repeatedly add predicates to it's currently best solution while trying to maximize the number of test cases which it had solved correctly.
There's probably some overlap with the different search strategies that can be applied to logic languages and Prolog-like systems. Further heuristics can limit the search space. Now we have programs that write programs!
For example:
Gives: