Language vision regarding safety guarantees

ia0:

I hope you see that your single contract is made of a logic part (with requirements and guarantees) and a safety part (with requirements).

Yes. But I wasn't talking about safety requirements, I was talking about promises. My sort example doesn't even have any safety requirements.

Safety requirements are an integral part of the contract. There is only one set of guarantees that the contract has. Safety requirements don't create two versions of the contract, they just provide a boundary to what the contract promises. There are no guarantees at all outside of the boundaries of what safety requirements require. It's just undefined behavior in that scenario.

But what you are suggesting is something completely different. You keep saying that there should be two different versions of the contract. One for purposes of "logic", and a different one for purposes of "safety", with different guarantees. That's what I'm disagreeing with.