Language vision regarding safety guarantees

I have more or less understood you. Is it equivalent to bug -- vulnerability, or incorrect -- unsound?

If so, I do think there is few necessity of logic contract. First of all, Rust cares about memory safety the most, and try to make logic correct with type system. Secondly, even if we have logic contract, we can''t guarantee that a verified program is logically correct, but only guarantee that it works as we expected within modelled logic contract.

And for safety contract, I still have my opinion:

If an unsafe operation requires post-condition of an upstream crate:

• If the safety "ensures" contract from upstream crate covers such requirement, you don't need to do anything.
• If not (either no safety contract or not cover), you must check it at runtime.

The above rules make it possible to fluently upgrade a dependency, and you don't need to review third-party code for contract, or worry about how unsafe downstream client uses your code (a library writer only need to care about the correctness of safety contract, and breaking changes of safety contracts across major versions).