doing research on usability of theorem provers is basically doing research on practical aspects of dependent types first 🙃 it’s exciting but exhausting
Conversation
What do you mean by “practical aspects”? Like in terms of how to implement them?
2
there are a set of features in functional programming that people would expect in dependently-typed functional languages and they're not (fully) available yet.
4
This Tweet was deleted by the Tweet author. Learn more
extensible records, effects, interfaces. also minor stuff like modules, namespaces, etc. the main question in my head at all times is "how can I make this ergonomic without breaking the theory?"
2
7
specially modules and namespaces that seem so trivial but they super matter if you don't want your future package manager to suck tremendously.
2
5
Yes I want nice modules so bad. Namespaces are also interesting but I don't understand them as much. Also interested in how stuff like staged computation interacts with package managers. Like it would be cool to be able to avoid depending on packages that have been inlined away.
1
2