The difference is that you can just use any kind of valid constrains or invariants to prove safety in C (but unfortunately these are just in mind or documentati

The difference is that you can just use any kind of valid constrains or invariants to prove safety in C (but unfortunately these are just in mind or documentation and not verified by compiler), while you have to fit to specific model of constraints used by Rust.