Will Crichton

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?

Yeah, agree! Otherwise small local moves can blow up the search and you don't know why Slight ironic that synthesis, which is used for producing more transparent algorithms than ML, suffers from this issue in its own search process

Synthesis research is usually about more powerful search, but perhaps a better framing is carving out a space of searches that make sense to a programmer.