New WG21 paper P4043R0: Are C++ Contracts Ready to Ship in C++26?

Reading a bit more, I think I see a glaring hole wrt multi-threading. Say x and y are atomic, then even [[pre(x.load(std::memoryorderacquire) < y..load(std::memoryorderacquire)] isn't one atomic operation and can lead to inconsistency (toctu like) issues. And this gets only worse when global variables/member variables are used within a contract. So in that respect using contracts may introduce a false sense of security in a multi-threaded environment and this is bound to cause issues in practice.

Reading further
I see this issue is kind of known/implied... and I would consider it a blocking issue for release.

Could be resolved by allowing (directly invoked?) lambdas, though that's kind of clumsy too
pre[[[]{std::scoped_lock mtx; return x < y; }]

I'm not sure what you're saying. My name is displayed on both Stack Overflow and the paper.

Nevermind, I edited the question.

An engineering process should always be optimized to detect engineering issues as soon as possible. For C++ anything you can move from runtime to compile time thus is something anyone should use. So yes I would definitely use it.

Contracts need to be precise and complete. And I have from long ago been exposed to formal correctness proofs which indeed have pre and post conditions AND invariants.
So no for me it doesn't need simplification (I haven't investigated enough to know if the pre/post conditions are expressive enough, but seems good enough to start with)

But all in all miss an explicitly named invariant attribute [[invariant: x > y]]
which could be used to further optimize generated code and/or prove its correctness.