You make a good point about proposal submissions, I submitted P4363R0 to propose a 5th, 'static' enforcement mode P4363
https://isocpp.org/files/papers/P4363R0.pdf
Interesting proposal. Having a way to mark a contract invocation as statically checked is a good idea. However...
1. It does not specify how the checking is done, leaving it to ephemeral "matter of implementation quality".
2. In its specification it offers zero guarantees, saying "Failure to establish that a predicate is satisfied does not make the program ill-formed." This is even less than current c++26 contracts offer, which at least have an implementation defined choice of modes, two of which guarantee not continuing into the code whose preconditions was broken.
3. It offers no current way to distinguish "fail" - ie, we proved the opposite, from "unknown" - ie, the analysis couldn't show it true. In the former case you'd likely want it to make the program ill-formed because it *knows* that it's broken, marking that as "diagnostic encouraged" would be weakening what compilers can already do with contracts.
4. The modeling of this request as a semantic has the problem that it is now chosen at the resolution of *checks*, not *invocations*. If we'd set such a check on a widely-used function, like std::string::find, that would either require checking in all places including those in our test tools, or forfeit checking those in our most critical string handling. It feels like the choice is on the wrong atom; it should be tied to the invocation scope or the specific invocation somehow.
5. The name could use some work. But I don't think it makes sense to discuss the name when there are more fundamental things to discuss.
May I ask, are there any reports from well known companies in Aviation, Medical or Automotive (eg ISO/SAE 21434:2021 – Road Vehicles) of the P2900 design?
The Automotive one requires consideration of secure programming techniques. I would be keen to read their findings.
Most of these areas are inherently extremely slow in picking up anything new; MISRA isn't considering looking at C++26 yet for a future release. Many automotive customers I know of are still on C++17 and not actively moving to C++20 either. Finding one, specifically ones that are interested in safety contexts, that are willing to consider what needs to be done is extremely unlikely. The secure techniques you're thinking of are most likely the area of ISO26262 / ASIL-C/D, which are very far from anything bleeding edge. In fact, I believe they're still using C, and likely C89 at that.
Having a good story why C++26 or 29 would be a much better choice for them is a great argument to get them to look.
My concern about at runtime contract models is there isn't Hoare Logic {P} C {Q}
It may sometimes be 3 execution commands in a row: PreCommand, Command, PostCommand.
I'd love to see a paper that effectively stops any modification from PreCommand and PostCommand. Or equivalently, one that specifies how to do the static analysis in an implementable way that uses Hoare's propagation. In fragments I can easily see how it works, but whole-function analysis runs into loops and recursion, both of which break many of the properties we want, or require continued analysis or loop summarizing of sorts. If somebody has the answers to those, I'd love to read all about it.