> Well, the easy answer is that dependently-typed languages like Agda and Idris aren't very mature yet. It's also self-evidently wrong. Agda was first released

> Well, the easy answer is that dependently-typed languages like Agda and Idris aren't very mature yet. It's also self-evidently wrong. Agda was first released in 1999, ten years before Go. If you use a wallclock interpretation of "maturity", Agda is twice as old as Go and Idris is roughly as old as Go. Both are used significantly less (by several orders of magnitude), though. Despite them having a far stronger type-system. If you, on the other hand, you are using a "developers' time" interpretation of maturity, on the other hand, you are making a circular argument, i.e. "Agda is seeing less use, because it has been used less", as resources invested in a language ecosystem tend to be strongly correlated with it's usage.