One of the largest issues with program synthesis right now is that it requires a lot of knowledge of synthesis to be actually used. Indeed, sometimes the synthesis will fail to give an answer due to underspecification, and only an advanced user with deep knowledge of the synthesis engine will understand where that underspecification lies. For that advanced user, it is easy to identify the underspecification, provide the required spec, and watch synthesis succeed. However, users who have the knowledge of that in general don’t need synthesis. While they can use synthesis for some small helper functions (I recently used synthesis for the generation of a cartesian map), the majority of the time those users aren’t the ones who can benefit the most from synthesis.
However, the synthesis engine itself is aware of when it’s underspecified. For example, during a case analysis, the synthesis engine can see that one of the cases is not hit through any of the examples. Guessing randomly in this circumstance is very likely to fail, and will very likely require some more user input to work. Then the user will need to go through the code, confirm that it was synthesized correctly or incorrectly, and think up the right example to specify that incorrect codepath. After that, they will need to rerun the synthesis algorithm from the start again, creating and subsequently pruning large numbers of potential programs before finally getting to the same place as before, and being able to now progress further.
Indeed, one could even see a scenario, when attempting to verify whether a program is one of two potential synthesized programs, running some static analysis on them, and using that analysis to provide an example input where the two programs deviate, and providing a user with a multiple choice about which output should be created from the input.
Lastly, one could see the potential for the user taking even more interaction. The synthesizer could provide examples of a general nature, for example, saying “consider running f on a::b, would you like to return a) a, b) f b, c) something else, d) depends on a, e) depends on b, f) depends on a and b. In this way, the user doesn’t need to understand syntax or how to code, but they can direct the program into the correct answer through their knowledge of how the code works. And it can direct through some of the hardest parts of synthesis, finding when case analysis needs to be applied.