On Mon, Oct 20, 2025 at 10:01 PM Ville Voutilainen <
ville.voutilainen_at_[hidden]> wrote:

> On Mon, 20 Oct 2025 at 23:57, Gašper Ažman <gasper.azman_at_[hidden]> wrote:
> >
> > I mean that the P2900 syntax is enough for assertions; inline semantic
> forcing IMO actually decreases safety (in the same way that to keep an
> exposed gas pipe safe, you should mark it loudly, and not try to build
> massive walls, because it statistically leads to fewer accidents).
>
> I don't understand how that answers my question.
>

The current syntax does not preclude the feature I think is useful; but it
is, alone, not enough. The P2900 defaults minimize P(issues) compared to
alternatives, in my assessment. A different weighing makes your conclusions
completely reasonable.


>
> > 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.
>
> Suggested massive investments tend to have bad chances of actually
> happening...
>

The current design does not preclude those at all. We will need a lot of
annotations to make the current ecosystem hardened; we need a whole other
algebra to make it provable. I'm just one of the people working on that,
but it's a completely different feature, and I have as of yet little to
show, so I'm not going to block a bird-in-hand that seems to work just fine
for what it was designed for.