On Tue, 21 Oct 2025 at 08:08, Tom Honermann <tom_at_[hidden]> wrote:
> >> We will need a massive investment into static analysis for the predicates to be useful for proving programs correct without runtime checks, which is where the real step-change will come from. In my opinion.
> > It's curious indeed that we didn't then choose an approach that would
> > actually help all that static analysis, and perhaps make that
> > investment less
> > massive.
>
> You've made such assertions before.

*yawn* I didn't make assertions then, and I'm not making them now. A
static analysis tool vendor
had a proposal, I asked what it means, and how it works, and why, did
some work to figure it out,
and asked another static analysis tool vendor to check that
figuring-out for correctness. The result of that
exercise is
https://open-std.org/JTC1/SC22/WG21/docs/papers/2024/p3362r0.html

> As someone who worked on a static
> analysis product for over a decade, I can say, without hesitation,
> unequivocally, that P2900 contract assertions are usable and useful for
> static analysis. Full stop.

And yet we need a massive investment into static analysis, and
extensions to the contract assertions themselves,
for them to be useful for proving programs correct. Gasper is right about that.

> > Suggested massive investments tend to have bad chances of actually happening...
> I believe the investment that Gašper is referring to is the application
> of contract assertions to existing/new software projects, not investment
> in static analysis techniques and technologies.

I don't believe that's what he's referring to. And I don't think it's
sound to work based on beliefs.