Hopefully my answer above makes this more clear. The high-level idea is that if you are going to take the trouble to specify the type of a function (as in Hask

Hopefully my answer above makes this more clear. The high-level idea is that if you are going to take the trouble to specify the type of a function (as in Haskell), and tests that use the function (as in unit testing), and high-level properties of the function (as in Quickcheck), you may as well try to get the computer to actually generate the function for you, rather than writing it yourself. You mentioned Coq above. Coq users rely on the `crush` tactic to try to fill in the boring details of a proof obligation. This is similar in spirit to search used in synthesis systems. If you can give the high-level specification, let the computer do the "boring" work. Of course, the boring work may be difficult or computationally expensive, and the high-level specification may be ambiguous...