Rust has the same level of rigour, other than lacking totality. Not having dependent types makes properties a lot more cumbersome and less practical to encode, but the actual proofs you get of the properties you do model are just as valid as those in Coq and Idris (modulo nontermination).
Dependently typed programming languages such as Coq and Idris let you write proofs about your programs. These languages are fairly academic, and most engineers probably won't find it worthwhile to use these tools. Personally, I love them. I wrote a short article about my experience with Coq: https://www.stephanboyer.com/post/134/my-unusual-hobby