Agreed, because the problem domain/system dynamics needs to be encoded into Scheme before synthesis can be useful for high level specs. If this kind of programming style takes off, it could possibly be useful for communities to supply "starter templates" for common patterns and system behaviors that they manually reason about all the time.
Yes, using templates for common patterns could be helpful. Or even using machine learning over existing code bases to infer such templates.
Similar to the use of templates is Matt Might's suggestion of using Barliman for code repair--given an almost correct definition of a function, and both passing and failing tests, try to massage the code to make it pass all the tests. I think templates could be useful here.
There are many approaches to synthesis, and Barliman's implementation is still very naive. Experiments by Michael Ballantyne and Greg Rosenblatt have shown that some synthesis tasks in miniKanren (used internally by Barliman) can be speed up by factors of thousands to millions (by restricting the grammar and using a type system, or by performing program specialization on the relational Scheme interpreter, as in the Mercury compiler). Alas, since synthesis is inherently exponential in terms of program size, a speedup of a million means that you can synthesize only a slightly larger expression. And the techniques Michael and Greg have used don't work for all problems, and can reduce the generality of the programs that can be synthesized.
Still, given how many synthesis techinques, tricks, and optimizations that we haven't tried, I'm optimistic that Barliman's synthesis can be improved enough to be practical for at least some uses. What those uses are, I'm not sure.
