My sense is that it won't really get close to meeting until dependent types are more mainstream. Idris is out there but not sure how usable it will end up being. Haskell and Dotty seem to getting closer even though I don't believe they entirely support dependent types.