Comment by gugagore

> they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it")

I understood you to be saying "bundling is encouraged", in the sense of

https://leanprover-community.github.io/glossary.html#bundled...

I'm not sure it's encouraged. I agree that it felt natural to define a type like NonNegativeInteger, or a wrapper type like `Sorted(T)` to indicate that that wrapped list is sorted. But I think this is an area of style and aesthetic that is still emerging, far from ossified.

The problem of "threading" new things within existing programs is an important one to address, and it has multiple solutions (context management, dynamic scoping (lol), implicit arguments, type classes). I am curious if the claim of "does not scale" is mitigated by one of those solutions...