Deductive verification of Rust programs