> Rust with its ownership type system goes one step towards more proofs.

Does it really, though? The ownership system only talks about ownership, which you only need to reason about due to the artificial choice of avoiding garbage collection. So yes, you get closer to proofs, but only to proofs of properties that are not necessary to prove for Java, say.

You might use the ownership and lifetime system to derive must-not-alias guarantees that might help with some verification tasks, but I'm not sure how much it would help.

I'd love to see a deductive verification system for Rust, but I wouldn't expect it to be the silver bullet for verification.