On Sun, Oct 26, 2025 at 8:37 PM Ville Voutilainen <
ville.voutilainen_at_[hidden]> wrote:

> On Mon, 27 Oct 2025 at 02:24, Joshua Berne <berne_at_[hidden]> wrote:
> > 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.
>
> It seems like there's a very good chance that we can get to a
> non-violent agreement here.
>

Anything is possible.



> Herb's axiom-corollary post is riddled with presumptions of the ilk
> "this is (the only thing) what static analysis should do, these are
> the things it can rely on,
> and then it always does this-and-that".


> And both of us say "no it isn't".
>

Yup.



> And I'm not saying "no it isn't, it instead always does this-and-that,
> and that's the only thing it should do". I'm saying "no it isn't,
> because there
> are static analysis uses that don't have those presumptions, it
> doesn't do what you describe, and it certainly shouldn't do what you
> describe".
>

Whether we agree on this depends on what that last "it" refers to. If it
is just referring to specific static analysis uses, then absolutely.
Another reading of that statement is that you are referring back to all
static analysis tools, in which case I disagree.

Herb did indicate that he expected there to be multiple tools that approach
things in different ways, and I think that's the important takeaway ---
there are very useful tools that make certain assumptions about code and
then give you corollaries based on those assumptions. There are other
tools that might be able to separately validate some of those assumptions.
 There are other tools that make different assumptions and give you
different bits of information about your code.

All of these tools can coexist, and all of these tools can benefit and
handle contract assertions to different extents.

None of them are going to find *all* bugs in a program within our lifetime,
so we aim to enable the ones that are most useful and effective at finding
the bugs that will actually impact our software.

Personally, the tool that tells me when my contract assertions will be
violated and doesn't make me waste time on branches after the violation is
incredibly useful. It lets me focus on making my software correct, and
devote time and money to improving the code that actually moves my business
forward. The more correct it is in that initial analysis that considers
contract assertions, and the more consistently i make sure I address all
issues brought up by such analysis, the less likely it is i ever need to
consider a program where a violation has occurred. (And at that point i
can make risk/benefit determinations to leave runtime checks in, or take
them out, or spend more time analyzing the code branches that would be
followed if a violation did happen to occur even when my tools are telling
me it has been made impossible. Different environments will end up doing
all of these things).