Conversation

Slightly tangential, but I'd love to find a reference for how type theory and types in PL developed independently, then were eventually combined later on:
Quote Tweet
History subtweet: I regularly see the claim that "type theory invented type systems": that we have static typing because people tried to apply type theory to programming. This is untrue. The two concepts developed independently and were unified much later.
Show this thread
1
3
Replying to and
This might be useful too? It's more about the current state of affairs though, than the history:
Quote Tweet
“What are we thinking when we present a type theory?” by Peter LeFanu Lumsdaine: youtube.com/watch?v=kQe0kn I found the clarification of some of the hidden rules you have in your head when reading type theories really interesting and worthwhile!
Show this thread
Image