Thanks! Yes, Barliman is ambitious. Both the synthesis capabilities and the interface will need to improve before Barliman might be useful for practicing prog

Thanks! Yes, Barliman is ambitious. Both the synthesis capabilities and the interface will need to improve before Barliman might be useful for practicing programmers. One question Barliman is trying to explore is whether relatively modest synthesis abilities might be useful for some tasks. If the last 10% of a function could be synthesized, for example, how useful would that be? Perhaps a better question is, "for which tasks, if any, would modest synthesis be useful"? I don't know the answer to this question. A tool like Barliman might be useful in an educational setting. However, this seems a bit like the calcular/Wolfram Alpha debate in teaching math. If Barliman becomes good enough to synthesize many simple Scheme definitions from examples, would that take away too many learning opportunities from students? I suppose it would teach students to think of example tests, and perhaps even properties, types, or contracts, for the functions they are defining. But it does seem that the better synthesis works, the less useful Barliman might be in a teaching setting. One suggestion from Matt Matt is to use Barliman for code repair. For example, say I define a function `foo`, along with several tests that `foo` passes. Later I find that the definition of `foo` is incorrect, and come up with several more tests that fail using the current definition. Barliman could have an "auto repair" button that attempts to synthesize a correct definition of `foo` from both the tests and the "almost correct" existing definition. I have several ideas of how this might be done. For autorepair (and other synthesis tasks) it would be helpful to extend Barliman to run synthesis tasks remotely--for example, on an EC2 X1 instance with dozens of hardware threads. For more advanced synthesis tasks, I think we'll need a more sophisticated search. I was very impressed with Alpha Go's performance over a giant search space that historically has been considered the domain of human experts, a task that reminds me greatly of synthesis. I'm working with Rob Zinkov and Evan Donahue on using stochastic search/Markov Chain Monte Carlo/etc. to try to allow miniKanren's search to explore more promising areas in the search space. One inspiring piece of related work is this 2013 ASPLOS paper by Schkufza, Sharma, and Aiken on Stochastic Superoptimization: http://theory.stanford.edu/~aiken/publications/papers/asplos13.pdf http://theory.stanford.edu/~aiken/publications/papers/asplos... I don't see Barliman or other synthesis tools replacing programmers any time soon, but in 10 or 15 years I hope our tools will be assisting us with useful synthesis tasks.