Wrote a longish comment on some of the issues with using dependent types in general programming: reddit.com/r/ProgrammingL - hopefully I didn't misrepresent anything! 😅
Conversation
Replying to
Thanks for mentioning the encapsulation problem! This was a big frustration to me when I realized it, and I suspect it might be the real, serious challenge to adoption after the “proofs? In MY code?” crowd fades away.
Replying to
Again I don't get the "abstraction boundary" complaint. In most languages, if you change a definition, you have to review everything which depends on it...
1
3
In TT, we can type an interface up to functional correctness, so it's possible to change a definition and not have to review *any* downstream code.
1
2
Show replies