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 testi

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.