However, not all program values can be easily lifted to solvers. So the goal with RbSyn is to allow the programmer to write the same tests they would have written anyway to check their program correctness, without any extra fiddling. As tests subsume examples, we expect more program behavior can be specified than just using simple examples.
> I do wonder if the benefit will really be significant enough to make it worth it.
I have often pondered on what makes a program synthesis tool useful. I expect writing code as art as much as it is science, and people like to express code in the way they model system behavior in their head. In that regard, I do not think program synthesis tools will enable you to automate away large parts of code, but I do think it will automate mundane parts of a program; like writing utility methods, or filling in a partial program when enough information can be gathered from surrounding context (such as the arguments you write for a substring function).