cognitive psychology. PhD 
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?)
-
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?)
Oh another relevant paper. "One λ at a time: What do we know about presenting human-friendly output from program analysis tools?" http://static.barik.net/barik/publications/plateau2017/tbarik-lambda-plateau2017.pdf …
