For the short term and mid term yes. However I do hope that in the long term the ideas from ATS, Liquid Haskell, Idris, F*, etc. will be iterated on in order to

For the short term and mid term yes. However I do hope that in the long term the ideas from ATS, Liquid Haskell, Idris, F*, etc. will be iterated on in order to make them more accessible and usable. In the mean time we'll probably start to see Rust graft on more and more correctness tools like dependent types and SMT solvers, and it will begin to get a little ungainly, like dependently typed Haskell is. But there's only so many ideas you can try out in a new language, and Rust has made the right decisions on that front in the interests of getting into production this decade. :)