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?)
-
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?)
-
-
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 …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
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?"
- Show replies
New conversation -
-
-
Very little has been done for tactic debugging, aside from defining the language so that it's easier to debug the tactics to begin with, and visualizing proof state before and after. It's a hard but important problem.
-
OTOH the best work I've seen for debugging OCaml type inference I think used solvers (Calvin, a UW alum), so I think synthesis will help more with that than the type inference lit will help with debugging synthesis.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.