The fact that it's a research topic really says all you need to know in my opinion. It's not a question of whether you can do it in principle, but rather whether it's an effective alternative to other approaches.
I agree, I don’t think dependent typing and validating the correctness of your program using formal proofs is ready for mainstream adoption. I think it might be ready for some domains, like aeronautics, where the cost of errors is very high.
