> 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.
[0] http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=4AD...