As far as I got :D

I don't know quite what as far as I git implies!

On Thu, 23 Oct 2025 at 17:55, Oliver Rosten <oliver.rosten_at_[hidden]>
wrote:

> For what it's worth, here's as far as I git (I haven't thought about this
> for a while, though):
>
> The point is to introduce a classification of contracts complimentary to
> wide/narrow that hopefully has some properties that are intuitive and
> helpful in practice. I've tried to lay this out slowly and carefully,
> though doubtless there are things that can be improved in the way I've
> written this and there may be oversights.
>
> Definition A: The essential behaviour of a function is defined through the
> observable effects corresponding to its primary purpose. A necessary
> condition for executing the essential behaviour is that all preconditions
> are satisfied.
> Example A1. The essential behaviour of std::abort is to abort your program.
> Example A2. The essential behaviour of float sqrt(float) is to return the
> square root for non-negative numbers.
>
> Definition B: The inessential behaviour of a function is any behaviour
> that is not essential.
> Example B1. The inessential behaviour of std::abort is the empty set
> Example B2. The inessential behaviour of float sqtr(float) is the
> behaviour for negative arguments.
>
> Definition C: The essential domain of a function is the set of inputs
> (broadly defined, since this could include global state) that elicits the
> essential behaviour.
> Example C1. The essential domain of std::abort is a void argument
> Example C2. The essential domain of float sqrt(float) is the non-negative
> floats
>
> Definition D: The inessential domain of a function is the set of inputs
> that elicit the inessential behaviour
> Example D1. The inessential domain of std::abort is the empty set
> Example D2. The inessential domain of float sqrt(float) is the negative
> floats
>
> Definition E: The essential image of a function is the set of observable
> state changes generated by the function operating on the elements of its
> essential domain
> Example E1. The essential image of std::abort is the program aborting
> Example E2. The essential image of float sqrt(float) is the non-negative
> floats (although there is some subtlety here aa not all non-negative floats
> can be reached in practice).
>
> With this in mind, I think this can be profitably applied to contracts by
> introducing the notion of a "faithful" concept. I'm borrowing from some
> maths terminology here but there may be a better term.
>
> Definition F: A contract on a function is faithful if and only if
> invoking the function for each element of the inessential domain
> - Returns control to the caller
> - Produces a behaviour not within the essential image
>
> Example F1. std::abort has a faithful contract (trivially, since it
> doesn't have any inessential behavkour).
>
> Example F2. sqrt, with a plain-language contracts stating that it is
> guaranteed to produce a negative number from negative inputs has a faithful
> contract.
>
> Example F3. sqrt, guaranteed to throw in case of negative input, has a faithful
> contract.
>
> Example F4. sqrt, guaranteed to return 42 in case of negative input does
> not have a faithful contract. This is because the output is in the
> essential image. In other words, without inspecting the input, there's no
> way of knowing something atypical has occured from the output.
>
> Example F5. sqrt, guaranteed to return NaN in case of a negative input is
> subtle. If NaN is included in the essential domain and we take sqrt(NaN) =
> NaN, then the contract is not faithful, since NaN is in the essential
> image. If NaN is not in the essential image - which I think is the more
> natural decision - the contract is faithful.
>
> Example F6. sqrt, guaranteed to abort in case of negative input is not
> faithful, since control is not returned to the caller. I think this is a
> desirable classification.
>
> Example F7. sqrt, whose behaviour for negative input is undefined, does
> not have a faithful contract. Control is not guaranteed to be returned to
> the caller, nor is the behaviour guaranteed to be within the essential
> image.
>
> Example F8. Imagine a future evolution of contracts where someone could
> write a (highly dubious) implementation of abort that looks like
> void std::abort() pre <always_enforced> (false) {}
>
> This does not have a faithful contract
> - Since the precondition is always violated, this function does not have
> any essential behaviour
> - The inessential behaviour is guaranteed *not* to return control to the
> caller.
>
> Perhaps where this classification is particularly useful is in cases F6
> and F8.
>
> - F6 has a wide contract but not a faithful one. I think the latter is
> helpful, since just talking of a wide contract in this case may be
> counterintuitive: although there is no UB, your program will crash if sqrt
> is called by a value in the inessential domain. Introducing a
> classification of contracts that reflects this seems useful to me.
> - Regarding F8 it's not clear to me, from first principles, whether it
> has a wide or narrow contract. It unequivocally does not have a faithful
> contract, which again points to the potential utility of this
> classification.
>
>
> O.
>
> On Thu, 23 Oct 2025 at 17:50, Ville Voutilainen <
> ville.voutilainen_at_[hidden]> wrote:
>
>> 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.
>>
>