Hm but isn't that how all static analysis tools, including Rust'a compiler itself, work?
I.e.: You know the function body is, according to some definition, let's say aliasing, consistent. You annotate the function signature, thereby expressing formal contracts for that function any caller has to fulfill; given the contracts are fulfilled, the function call will then be consistent.
Meaning, you prove the function body is consistent, you annotate the function, and you then get the guarantee that the function is correct for any callsite that fulfills the contracts. If you want to prove this using a formal prover, you have to annotate the function, and annotate the callsite in such a way that the prover can prove that the contracts are kept, AT THE CALLSITE.
Isn't the difference in it being required, and opt-out (unsafe) in rust, but opt-in here? Also, my understanding is the rust compiler guarantees "soundness" in safe rust, so it checks and validates that the function signatures (with annotations like lifetimes) are correct
I.e.: You know the function body is, according to some definition, let's say aliasing, consistent. You annotate the function signature, thereby expressing formal contracts for that function any caller has to fulfill; given the contracts are fulfilled, the function call will then be consistent.
Meaning, you prove the function body is consistent, you annotate the function, and you then get the guarantee that the function is correct for any callsite that fulfills the contracts. If you want to prove this using a formal prover, you have to annotate the function, and annotate the callsite in such a way that the prover can prove that the contracts are kept, AT THE CALLSITE.
Or am I missing your point?