Language vision regarding safety guarantees

Evian-Zhang:

@ia0 feel free to correct me if the examples don't represent the problem

Those examples are fine, but they are more complex than needed. There's no need to have traits involved. A more simple example (following the generic pattern of the original post) would be:

• Some math crate provides a GCD (greatest common denominator) function.
• Some game engine crate uses it in unsafe code (games are fast) for coordinate alignment.
• A binary implements a game using the game engine (unaware of the math crate below or the unsafe code).

Evian-Zhang:

One can never image how the downstream users use this function's output contract.

A crate author doesn't need to imagine anything. A crate author has an idea of a functionality they want to provide (e.g. sorting slices). They provide a first version with a postcondition they believe is useful. If it's not always useful, they're gonna get feature requests (e.g. the sort should be stable). So building a postcondition (or guarantees) is an iterative process. Actually building the whole contract is an iterative process, because requirements may be too strong for some users.

Evian-Zhang:

In my point of view, it is meaningless to talk about whether an "ensures" contract is for safety or for logic.

I'm not sure how you reach that conclusion. Is it because "ensures" are meaningless in general? (which I hope I addressed in the previous quote) Otherwise the distinction is what the crate author wants to guarantee for which purpose. To take the sort example again, the crate may choose to guarantee a stable sort for logic and a permutation for safety. Or anything else. This will be discussed with its users through feature requests (or pull requests if it's just about documenting something the implementation has always been doing).

For some reason the rest of your reply is on point, so I might just have misunderstood that initial segment. Although I consider the notion of verification out of topic for this thread. My problem is the lack of freedom in the safety contract, which prevents encapsulation of the scope of unsafe for dependencies.

dlight:

Well there is a better approach now that we have some verification tools

I'll clarified in the original post that this thread is not about how safety contracts are verified, but what they should contain. Verification is a different topic.

dlight:

bar should depend on a very specific version of foo

In that case you're just making foo and bar in the same unit of implementation, which indeed removes the problem because there's no need for contracts. But that's just ignoring the problem when they are in different units of implementation (when bar only sees the contract of foo not its implementation).

dlight:

That's because if some unsafe code depends on some safe code to not trigger UB, then the author of the unsafe code should review the safe code thoroughly.

This has been debunked in Conditions for unsafe code to rely on correctness, unless you know of an official language statement that says this is not the case. But I agree with you that this convention is dangerous and the core problem this thread originates from.