Unwinding assignments into a single-assignment notation is common in verification. (We did it automatically 30 years ago in the Pascal-F verifier.) Rust is expressive enough that you can do that in Rust itself, which is convenient. It's not "functional" that's important for this; it's single-assignment. Each variable in the proofs can have only one meaning, because the proofs have no notion of time. (Well, there's temporal logic, but you don't need to go that route.)
Whether you should trust the compiler is always an issue. When we did this, we verified at the stack-machine level. At that level, operations are like "pop two operands from stack, add in 16 bit integer mode, push result". At that level, semantics are relatively simple. If you have the compiler's dictionary available, you can give names to all those things being pushed and popped, much as a debugger does.