While there are/were several languages with dependent types, like Agda, Coq or Epigram, none seemed to gain wider adoption. Despite that dependent types allow very strong type safety, up to writing complete program specifications. Did anyone analyze what are the main blockers for such languages to become more mainstream?
4
It’s not enough for a language to have a nice feature, it also needs a compelling application. For example, functional programming languages didn’t really take hold commercially until the growth of big data in general and Scala and Apache Spark in particular, and it is still largely limited to those niches.
Personally, I think dependent typing’s “killer app” is its potential for tooling. If you’ve ever watched one of Edwin Brady’s Type-driven development talks, you’ll know what I mean. He can write a type signature, then hit a few shortcut keys to write the function body. With some refinement and UX, I think that could make dependent typing a must-have language feature at some point.