[elcritch]

Wondered that myself. It’s surprising there’s not more languages with dependent types (and the associated requisite libraries).

I suspect it’s taken a while for the theory behind dependent types to become widespread enough for some enterprising hacker or grad student to make a useable language for them (e.g. Idris). Even if a new theory comes along it takes time for appropriate metaphors and methods of using them to be created and disseminated.

Though does computing the dependent types at compile time take more process.