On 6/4/25 7:56 PM, Ville Voutilainen via Std-Proposals wrote:
> On Thu, 5 Jun 2025 at 02:15, Tom Honermann<tom_at_[hidden]> wrote:
>>> Relying on a hypothetical assume semantic doesn't help, especially
>>> because using that makes it not the same program, the compiled-altered
>>> program
>>> has different semantics.
>> The semantics are only different, discounting side effects of contract
>> predicate evaluation, if an assume semantic is violated.
> Which itself means that the semantics are different. They are
> different in exactly the same way
> as
>
> switch (foo) {
> case 1: bar1();break;
> case 2: bar2(); break;
> case 3: bar3(); break;
> default:std::unreachable();
> }
> code_that_follows();
>
> and
>
> switch (foo) {
> case 1: bar1();break;
> case 2: bar2(); break;
> case 3: bar3(); break;
> }
> code_that_follows();
>
> are different.
>
> And then, when there is a contract annotation that doesn't change the
> well-defined/undefined behavior sets of a program, and an annotation
> that does,
> they *should* be different, in source code.
>
> Thank you very much for this discussion. It crystallized the above.

You are welcome, but I don't think we've reached a conclusion here.

The semantic difference you describe seems just as applicable to the
ignore and observe contract semantics with the std::unreachable()
portion corresponding to code that is only reached when a contract is
violated. SG21 discussions occasionally considered requiring a
"continuable" annotation for the observe semantic, but it never got much
support because the ignore semantic exists. Do you believe we should
require an in-source annotation for the observe semantic?

I view contract semantics as a choose-your-own-adventure-story for the
behavior of contract violations:

  * *quick-enforce*: always well-defined, program terminates.
  * *enforce*: always well-defined, program terminates unless the
    violation handler throws, calls longjmp(), etc...
  * *observe*: library UB (which may lead to core language UB) unless
    the violation handler throws, calls longjmp(), etc...
  * *ignore*: library UB (which may lead to core language UB).
  * *assume*: always core language UB.

Tom.