> I think this is only true because there isn't a production-ready dependently typed language [...]

Now this I definitely agree with. I want to see what's possible!