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
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
I think it's a statement about things like changing which argument + pattern matches on, which can break proofs downstream, even though it would be innocuous in other languages.
2
2
I guess a plausible fix would be the ability to export a binding from a module without exporting its inductive/recursive definition. That way, people wouldn't accidentally write proofs using the inductive structure of +, and instead compose theorems proven in the Nat module.
1
2
Yeah, I mentioned how changing the function definition of + can break client code, even if the type signature does not change. This is a pretty weird default behaviour for most programmers!
1
1
1
Perhaps it’s not too hard to solve though, if definitions were simply made private by default. I’m not really an expert on this stuff though!