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?)
-
-
Replying to @geoffreylitt1 reply 0 retweets 1 like
-
Replying to @maxkriegers @geoffreylitt
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 …
3 replies 0 retweets 8 likes -
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?)3 replies 0 retweets 3 likes -
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
2 replies 1 retweet 3 likes -
Replying to @geoffreylitt @wcrichton and
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?"
2 replies 0 retweets 1 like
I remember having this convo at PLATEAU, forget if it was with @barik /Will or other ppl. An analogue I came up with then was Active learning https://en.wikipedia.org/wiki/Active_learning_(machine_learning) …
-
-
Replying to @maxkriegers @wcrichton and
Yes, this just reminded me of this awesome Microsoft paper, which uses active learning and is related to helping the user understand the search https://www.microsoft.com/en-us/research/wp-content/uploads/2015/11/uist15.pdf …
0 replies 0 retweets 1 likeThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.