Will Crichton

Is anyone aware of program synthesis research on better error messages, so you can figure out how to improve your spec if synthesis fails? (perhaps related to better type errors?)

@wcrichton

Survey of error message research: https://dl.acm.org/doi/pdf/10.1145/3344429.3372508 … Nothing in there about synthesis. The only HCI-esque work that's been done on synthesis (to my knowledge) has been for programming by example: https://www.aaai.org/ojs/index.php/aimagazine/article/view/2262 …

But @geoffreylitt I think your intuition is correct. If you knew the best way to help someone e.g. debug H-M type inference, that's a step to general synthesis. Another place to look would be debugging tactic programs in a proof assistant (maybe @TaliaRinger knows lit here?)

thanks, helpful pointer. also enjoyed your PLATEAU paper! context btw: playing with Synquid for a class (synthesis w/ refinement types, http://comcom.csail.mit.edu/comcom/#Synquid ) neat tool, but specifying w/ types is subtle and challenging, and error messages are often unhelpful

i'm still very new to this area but producing good errors seems hard.. "you've failed to specify some constraint on a value, which is causing our search to fail... think, what implicit constraint is in your head which you haven't written down yet?"

Seems to stem from a fundamental belief in synthesis that it should be black box. Input spec, output program. But in practice, you *always* have to know how the algo works to do anything interesting. Maybe focus should change from good errors to algorithmic transparency?