Hi Sebastian,

On 2026-05-22T00:42:26+0200, Sebastian Wittmeier via Std-Proposals wrote:
> That would make the diagnosis dependent on the quality of the
> "prove engine", of the compiler or static checker settings, possibly
> of half-unrelated parts of the program (e.g. one indirection more).

That's why I said it should probably be just recommended practice, and
not a mandatory diagnostic. That way, when compiling with a dumb
optimizer, you could turn off the diagnostic, and when compiling with
a powerful one, you could turn it on.

Of course, the programmer should only use the trap statement
judiciously, and shouldn't use it if/where it expects that it will have
too many false positives. If a programmer wants the program to abort
without diagnostics, we already have the abort(3) function. The trap
statement would be a sharp tool for this use case.

> Just saying. That all could be okay and reminds of automatic checking for C++ contracts.
>
> One approach could be that a tool that first proves some "fact"
> creates some machine-only- or also user-readable marking how the proof
> was done. So other systems can revisit the proof, even if they are
> less sophisticated. That would give more reliability and stability.
> And it would also give (more) suitable error messages, if the proof is
> not viable anymore after a change in the code.

This is all implementation-defined. Off-topic for the standard, IMO.


Have a lovely day!
Alex

>
>
>
> -----Ursprüngliche Nachricht-----
> Von:Alejandro Colomar via Std-Proposals <std-proposals_at_[hidden]>
>
> trap; // diagnosed unless proved unreachable.
>
>

> --
> Std-Proposals mailing list
> Std-Proposals_at_[hidden]
> https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals

-- 
<https://www.alejandro-colomar.es>