[dwohnitmok]

Dependent types aren't terribly complicated intrinsically, see e.g. https://shuangrimu.com/posts/language-agnostic-intro-to-depe... for one explanation of dependent pairs.

Nor do I think the value of dependent types comes from proofs, which I agree are still too cumbersome to really use at a large scale for most codebases.

My hypothesis for the sweet spot for dependent types is to express invariants, and then use other mechanisms such as property tests to check those invariants, rather than actual proofs (except for trivial proofs). This does mean that I favor a very proof irrelevant style of dependently typed programming (i.e. in the language of Agda, way more `prop` than `set` or in Idris lots of zero multiplicities for dependently typed arguments) which is quite different from the way a lot of current dependently-typed code is written.