3/ And good type systems (OCaml, Rust) can check surprisingly useful properties while preserving all 3 of those benefits. Other FM approaches (eg model checking, abstract interpretation) can check even richer properties, but you lose out on other axes...
-
Show this thread
-
5/ Also relates to my advisor Daniel Jackson's work on "lightweight formal methods." When you work in Alloy (http://alloytools.org/ ), you're in conversation with the tool, sketching out a model, gradually refining. Speed is critical for that interactive workflow
1 reply 0 retweets 1 likeShow this thread -
6/ As other PL techniques get faster, new possibilities will open up for interactive tools... For example,
@webyrd is building an IDE with live program synthesis built in. Autocomplete on mega steroids
https://github.com/webyrd/Barliman 1 reply 1 retweet 9 likesShow this thread -
7/ Of course, speed is necessary, not sufficient. Wrangling terrible compiler errors still sucks even if they're fast. But with thoughtful design, it seems like types and other lightweight formal methods have a key role to play in the future of programming environments
1 reply 0 retweets 0 likesShow this thread -
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!
1 reply 0 retweets 0 likesShow this thread -
Replying to @geoffreylitt
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?
2 replies 0 retweets 2 likes -
Replying to @wcrichton @geoffreylitt
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.
1 reply 0 retweets 0 likes -
Replying to @wcrichton
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?
1 reply 0 retweets 1 like -
Replying to @geoffreylitt
Yeah, that approach turns it into a data vis problem. Probably want some kind of Google Map-esque zooming approach, viewing at different layers of abstraction. Very similar to how hw engineers use visual layouts for designing/debugging whole chips vs. individual components.
1 reply 0 retweets 1 like
At OPLSS, I was talking to someone about usability of theorem provers. IIRC they said when their prover failed, they would open the hidden text logs to see the proof tree it spit out and find the offending node. That was the signal for where to start fixing the proof.
-
-
Replying to @wcrichton @geoffreylitt
More generally, we **have** to move beyond ASCII diagnostics. We can push termcolor, ncurses, etc. to their limits but eventually we will need interactivity, direct manipulation, functional reactivity, etc. in our error messages.
0 replies 0 retweets 2 likesThanks. 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.
cognitive psychology. PhD