On Mon, 17 Aug 2026 at 15:22, Jonathan Grant <jgrantonline_at_[hidden]> wrote:
> > I have an implementation of the P2680 "strict contracts", of "symbolic
> > contracts" that we don't yet have a proposal for, and various forms
> > of static analysis for both. I'll eventually write papers describing those.
>
> I would be pleased to read those.

I'll likely have a function pointer contracts and a virtual function
contracts paper in the next mailing.
I expect to publish the analysis-related ones a bit later. But we'll
see, that sequencing isn't set in stone.

> > As for your compile_assert, based on the implementation of the
> > aforementioned, I have the means to prototype-implement it under any
> > proof-requirement rules you like. Not as "just give a result based on
> > whether the compiler was able to optimize-prove this is a constant"
> > like it is now, any rules.
>
> Interesting, do you have control-flow analysis?

Yep.

> I like it when the compiler proves, because I know the proof is valid for the machine code generated. If using a separate tool, we would be unable to state it was proven by the compiler that generated the compiled program.

We'll see how it goes. Sometimes such analyses are better done with
plugins, some might prefer a tool separate from compiler.
Some might prefer the compiler just doing it.