[KirinDave]

It's not even really possible to "adopt" dependent typing today. It's only emerged from the realm of academic curiosity and only two implementations exist that are anywhere near "practical" in the context you're describing.

Both of those implementations are very honest about their shortcomings, and nearly every talk and blogpost for them mentions you can't yet use this in many industrial contexts.

It's very difficult to see this as anything but the usual distate for PL theory that constantly swirls around this community. If the author didn't intend to associate a post with that, then they've done it by accident.

[ernst_klim]

>only two implementations exist that are anywhere near "practical"

Out of curiosity, why F* or Idris are not practical?

[KirinDave]

F* and Idris are precisely the ones I had in mind, although I guess you could make an argument for Agda.

What did you think I was imagining? I can only name 5 DT languages off the top of my head.

[ernst_klim]

So, why are they not practical in your opinion?