Yes, specifying behavior can be tricky. But I think there are ways to make it manageable. And, if you think type annotations, unit tests, property-based testing (as in Quickcheck), or contracts are useful, you are already specifying behavior in ways that can be used for synthesis.

I hope that future versions of Barliman will allow for the programmer to specify arbitrary mixtures of optional type annotations, tests/examples, properties (as in Quickcheck), contracts, etc. All of these specifications would be optional--if the programmer doesn't specify any of these, then Barliman would just act as a code editor. Heuristics such as parsimony (picking the smallest program that meets the specification) might help for ambiguous specifications. And stochastic search or machine learning might help Barliman search for programs that, according to some measure, look like existing Scheme programs, for example.

Since the programmer is filling in the code, while Barliman checks for compatibility and tries to synthesize code in the background, both the synthesis and the specification problems become more tractable as more of the code is filled in by the programmer. Features like "auto repair" (suggested by Matt Might) could take a fully instantiated program that passes some, but not all, tests, and use that program as the basis for synthesis. I think that specification is a challenge, but I think it a tractable problem, as long as you don't insist on fully unambiguous specification, which is a much harder problem.

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.

So is this like a simpler interface for making Coq-like specifications?