Articulating the ineffable. Programming language theory 
cognitive psychology. PhD @Stanford
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
8/8 I still have a lot to learn about types and formal methods, so I'm curious to hear thoughts on all this, or pointers to related ideas/readings!
Underexplored area IMO: usability of type inference. More sophisticated type systems become, more complicated the inference. HM-style is already hard to understand. What about when your SMT solver fails?
Inference is supposed to be a black box. But when it fails, the user inevitably needs to know how it works to avoid trial and error. These systems need to be able to explain themselves, interactively teach their mechanics.
Yeah, I really like the idea of allowing the user to pop the hood. Could be fun to try a naive thing like just show a graph representation of the constraints. Probably horrifyingly large for real programs, but maybe you can prune? And then link to the source somehow too?
Yeah, was just thinking about locating type errors: * are there better heuristics for localizing? * could you use edit history to inform the guess? the error is probably in that new code you just typed... * could visualize the constraint set to help user figure out the issue?
Apparently I need to learn what a bidirectional type system is...pic.twitter.com/CBq1XvZgBS
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
