My feeling is that dependent types add complexity to a language that's already well-known for having a complex type system, so I'm nervous about blowing the complexity budget. But I'm bullish on tools like Verus, Prusti, and Creusot because they allow people who need to write low-level unsafe code to prove their code safe, while keeping the complexity of the safety proofs localized to that code, so most Rust programmers don't need to worry about it. This allows verification of Rust code without surfacing complexity to most developers. We can have our cake and eat it too.

Agreed. Rust is on track to becoming a practical language for many verification projects. If necessary, perhaps a dialect that focuses on verification could be made and separately maintained (it would probably cut out a lot of normal Rust), or one would just switch to a different technology.