Yeah, when it comes to safety ("functional" or otherwise), angelic semantics is not what you want to reach to. Rather, you want to be looking at demonic semantics.

-- Gaby

-----Original Message-----
From: SG15 <sg15-bounces_at_[hidden]> On Behalf Of Ville Voutilainen via SG15
Sent: Monday, October 27, 2025 11:51 AM
To: sg21_at_[hidden]
Cc: Ville Voutilainen <ville.voutilainen_at_[hidden]>; sg15_at_[hidden]
Subject: Re: [isocpp-sg15] [isocpp-sg21] P3835 -- Different contract checking for different libraries

On Mon, 27 Oct 2025 at 20:39, Charles-henri Gros via SG21
<sg21_at_[hidden]> wrote:
>
> As a developer of static analysis, I can state the following:
>
> I'm not trying to prove anything, however nice that would be. Proving almost anything in the presence of pointers or loops is largely impossible (see Rice's theorem).

I have static analysis tools that prove absence (or presence) of UB.
With limitations, and with configurable effort spent. The static
analysis tools
that my company sells don't seem to do that, but the tools of at least
two competitors (and, in various areas, partners and suppliers) do.

I want them to do more of that.
_______________________________________________
SG15 mailing list
SG15_at_[hidden]
https://lists.isocpp.org/mailman/listinfo.cgi/sg15