On Mon, 27 Oct 2025 at 01:23, Herb Sutter via SG15
<sg15_at_[hidden]> wrote:
> Axiom: A fundamental property of contracts is that they are redundant – they never change the meaning of code.

That axiom doesn't hold to begin with, unless you have contracts that
are guaranteed to have such a property.

Such as contracts that are guaranteed not to have side effects.

For contracts that are not guaranteed to have side effects, it is then
not axiomatic that they don't change the meaning of code,
and such a non-existent axiomatic property cannot be relied on by
analysis tools. Which then means that given a call of function f()
in a predicate, you need to go and look at the definition of f() to
see whether it changes the meaning of code.

> Corollary: A program that runs successfully with contracts enforced should also run with the same meaning with contracts ignored.

Yeah, "should".

>(From this comes “assertions should not have side effects” which is taught in every assertion facility in every language I know of.)

Another "should", which isn't a property that can be relied on, so
needs to be double-checked.

> Corollary: A tool that analyzes the non-contract (“ordinary”) code should always analyze the correctness of the body ignoring contracts (or, equivalently, assuming contracts are ignored).

..seriously wondering what the goal of such a tool is. "I looked for
bugs in your code and presumed a whole bunch of things,
and based on those presumptions I came to the conclusion that your
code doesn't have bugs."

And then it can still have bugs, when those presumptions were incorrect.

> So in the above example, I would expect:
>
>
>
> (1) A tool that analyzes the function body would _always_ issue a “does not return on all paths” warning (and all compilers do: https://godbolt.org/z/TebeM1cdc). To silence the warning, add “else std::abort()” “else throw something{};” or or similar. This is right, because the function can indeed be called out of contract, and if so cannot just fall off the end.

And then, if you, instead of "pre(i<128)", have some "pre
always(i<128)" there, the situation changes.

Which is the whole point of such a facility. Human readers and tools
alike don't have to issue the warning you speak of. That warning
doesn't need to be silenced. There's no need for such a warning,
because we know that such a situation simply doesn't come up.
It doesn't maybe sometimes come up sometimes not, it never comes up.

> (2) A (possibly different) tool that also analyzes contracts would _additionally_ issue a warning if it discovers code paths that would violate the precondition. Contract-related warnings are purely in addition to, not instead of and not interacting with, other warnings.

A facility that is geared for giving more opportunities for issuing
warnings that by nature have false positives and false negatives
isn't much of an addition to our toolboxes. A facility that can help
tools construct proofs would be.