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.
>