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!
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!
1