1/ One of the most interesting insights from taking a program analysis class: I used to think type systems were just a way to restrict the values of variables... But you can also view them as a super-lightweight formal proof system! That can check many useful properties
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?
-
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?
- Još 1 odgovor
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.


