On Thu, 23 Oct 2025 at 19:43, Oliver Rosten
<oliver.rosten_at_[hidden]> wrote:
>>
>> .. ..but the.. ..philosophical width of it isn't wide,
>
>
> I agree with this. I think there's a gap in our terminology.
>
> I was actually discussing this with a few people off-list some months back. We didn't come to any agreement, so I don't want to pretend that what I'm saying has some sort of broader support.
>
> However, I proposed the notion of a faithful contract. I borrowed the name from the mathematical literature e.g. a faithful representation of a group. Full disclosure: Alisdair doesn't like this name but for now I don't have a better alternative and don't want to litigate that here. The name's not important.
>
> But I think we need some terminology to distinguish
> 1. A contract that is wide in the sense of no UB from
> 2. A contract which will guarantee that your program will crash for certain inputs.

I would suggest looking at (2) from the perspective of "a contract
which will guarantee that the code (either the function it's attached
to,
or just code that comes after, for a contract_assert) that follows it
is not entered if the contract is violated".

Because whether that crashes is a completely orthogonal consideration.
And.. ..there are contracts where what they're checking
for doesn't necessarily count as 'input'. At least not obviously so.