On Sun, Oct 26, 2025 at 7:35 PM Ville Voutilainen via SG21 <
sg21_at_[hidden]> wrote:

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

So build and run tools that do validate that particular contracts have your
desired property. Or don't check and rely on your coding standards to
achieve the same goal. How much you have faith in the "axiom" herb stated
is based on how much you have faith in your developers to have not written
very bad contract assertions and how much your tools warn you when you
might have contract assertions that have such problems.

Or apply static analysis tools only to a specific build with a specific set
of evaluation semantics.

Or apply them twice to both the build with all assertions checked (which
will tell you when you have issues that you have identified as incorrect
because you've put in contract assertions saying they are incorrect) and
then again to be sure nothing slipped through the cracks because of
differences in your production releases.

There are many ways to analyze code with contracts --- all aided in being
more useful because the contracts are actually written out in a way that
the tools can understand --- and each way will benefit different users and
use cases to different amounts.

Personally, I would prefer tools that let me focus on making sure that when
i run my code there will be no contract violations. If it can prove that,
then any time spent on the code paths where there have been contract
violations is just a waste of time.

I also want the fallback to say "ignore all of the contract assertions and
tell me if there are any significant problems in this particular build" ---
but that's a case of analyzing a particular build because it might be
heading to very sensitive environments or because i am attempting to
diagnose a problem that has been reported.

Lisa's talk from last year's evening session was very good at conveying the
different viewpoints from which one might approach a program with
contracts, and static analysis tools can and will be written to aid both of
those viewpoints.


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

Every static analysis tools takes as a given a certain baseline set of
ambient assumptions. It is only a compiler that must be limited to those
assumptions that are guaranteed by the Standard --- static analysis tools
frequently accept additional guidance regarding what they should and
shouldn't be focusing on (such as disabling particular warnings locally, or
implicitly by being applied to a build with NDEBUG not defined even though
a release build will have NDEBUG defined).

These ambient facts can and should include instructions on how that tools
should be treating contract assertions. Such facts can also be locally
verified when each individual contract assertion is being analyzed, with no
need to do it repeatedly in every user of a function.


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

A facility that requires checks always be run is a facility that will be
actually deployed less and less the more successful a library becomes,
which is directly counter to correct use of that library and means bugs
will eventually creep back in.

Note, also, that a runtime violation is never a false positive --- although
the bug might be because of the predicate itself being buggy. We can't
define a language where bugs cannot be written, so that is a fact of
reality that it would be nice for people to accept.