I'll cop to the word "viable" doing a lot of heavy lifting there, but I have not yet seen a dependent typing system that is adequate for engineering work. There are research systems, yes, and there are many people doing laudable work on it, but when people on HN pine for "dependent type systems", I think they're talking about wanting to live in a world where most people who are programming today are instead programming in dependently-typed systems happily and productively, not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.
Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.
> not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.
Well, to be fair, I would not cry if this happened.
> Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
1. Unfamiliarity with the standard library, tooling etc. I didn't expect Applicative to be in mathlib not batteries, for example.
2. I tried to prove things I wouldn't have in the Haskell version
If I knew the standard library, and did plane old arbitrary-length lists and partial (bounds-checked) indexing with arbitrary nats, I would have had less fun, but also done things way faster.
I am excited for the latest Machine-Learning tactics or whatever too, but the idea that "everything is going to do something they didn't before (proofs) and it will be no harder" is not a goal I am aiming for. Proofs will always be a trade-off between up-front costs and fearless refactoring on an ongoing basis. That's OK! I don't expect magic, I just want my programming language to give me the full spectrum of options, and then I can make my own economic decisions.
Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.