Sorry for the slow reply. As I understand it, Solar-Lezama's approach is based on CEGIS (counter-example guided inductive synthesis), using a model checker or

Sorry for the slow reply. As I understand it, Solar-Lezama's approach is based on CEGIS (counter-example guided inductive synthesis), using a model checker or similar tool to generate counter examples from a specification. Barliman currently doesn't use anything like CEGIS, although I hope to add something similar in the near futures, perhaps using optional properties (as in Quickcheck) or contacts as partial specifications. The sketching approach seems to require more structure than does Barliman in terms of what the programmer must specify, to make synthesis more efficient. The versions of Sketch that I've seen don't have anything like an interactive editor--the interactivity is really the key part Barliman is meant to explore. Solar-Lezama's group is doing lots of interesting work in addition to Sketch: http://groups.csail.mit.edu/cap/ http://groups.csail.mit.edu/cap/ I'm looking forward to trying to incorporate their techniques into Barliman!