lobsters score: 9 · tags: c++
“P-Members having abstained are not counted in this vote.”
How are abstentions even allowed? Either you’re a participating member and that comes with the responsibility of voting, or you step down as participating member?
score 1 · canonical
At least from what I can find P-members are indeed obligated to vote, but ISO explicitly states that “Abstention is a valid vote”. Presumably this is intended for cases where a P-member is indifferent to the vote outcome or for which there is insufficient internal consensus to vote one way or the other (as is apparently the case for at least some NBs).
Also one other thing to note is that for this specific ballot votes are cast by national bodies, which are themselves (usually) made up of multiple people.
score 1 · canonical
Contracts without neither proofs nor a strong type system make no sense, so C++ contracts are mostly useless. Compare these to Ada contracts, which are very well-designed, and can be used to prove things (e.g. no exceptions at runtime, allowing you to remove checks) given you can express side-effects. It is also distinguished between static (compile-time) and dynamic (runtime) predicates.
Who would spend all the time necessary to add contracts to a piece of C++ software? Given how deep you have to think of the code, you might as well rewrite it in another language.
Maybe it’s time to stop trying to tack on features to a language that is just not made for it.
score 2 · canonical
Ada has been around for a long time and is a good example. In Rust, Verus provides a newer implementation of the same vision.
There’s no reason that C++ couldn’t have had contracts like this. But defining a subset of the language for formal verification was declared explicitly out of scope.
In another direction, Erlang-style guard clauses provide a nice way of doing things like adding dynamic type guards and forwarding to specialised implementations depending on run-time properties (with the option of optimisers specialising the dispatch if they can prove a call site meets the requirements). But having dispatch influenced by contracts was explicitly declared out of scope too.
M# found that you could get some interesting speedups by inlining contracts at the right point to allow them to both be erased because they could be statically proven to always hold and become assumptions later. The requirement to support different contract enforcement policies across compilation units makes this impossible.
So we end up with a design space that has a number of interesting and useful design points and C++ picking a place that very carefully avoids intersecting any of them.
And then we’re told that people who criticise contracts aren’t engaging in good faith.
And then we end up with a situation in which we have a minority that is pushing contracts, a minority that has looked carefully at contracts and finds the design riddled with flaws, and a majority that believes the claims of one or other group and we’re told that this is ‘consensus’ and the design is pushed into the draft. And then people are surprised when the ratification isn’t unanimous.
score 1 · canonical
Thank you for your perspective! You mentioned that C++ could have had contracts like that, but I am not sure about this, given the gritty details of side-effects, for instance in multithreaded applications.
score 1 · canonical
Contracts that can be used for formal verification can’t have side effects that extend outside of the verifier’s abstract machine. The first thing that you need to do is define a subset of the language that is amenable to formal verification. C++ already, in the form of
constevaldefines a subset that can be evaluated at compile time with an abstract notion of memory. The contracts group explicitly declared defining such a subset as out of scope.The other side is that you can’t prove arbitrary properties and that the set of properties that you can prove in the presence of arbitrary aliasing and concurrent mutation may be small. This is true, but you can at least provide building blocks that let people prove that their program sufficiently constrains aliasing such that it can prove properties that they cared about. Verus manages this in Rust’s
unsafesubset but we don’t get the experiment to see whether C++ could benefit from this because the contracts folks declared it out of scope.
score 4 · canonical
Do you have a link to M#? I guess it isn’t the M# rapid application development environment, because that seems unlikely to do something innovative with lightweight formal methods…
score 1 · canonical
M# was the C# dialect used for Midori. Microsoft never published anything about it, though there are a few blogs. I consider it relevant because the WG21 convenor at the time P2900 was accepted was intimately familiar with it.
score 1 · canonical
I figured it would be that. I remember Gavin Bierman telling me stories about it when we were both at Oracle.
score 1 · canonical
I would assume it’s the C# for system programming attempt. I’m not sure how much of that ever escaped MSR.
score 1 · canonical
From looking around, it seems this was due to controversy regarding contracts? It almost seems like a political split going on there, with some people blaming the standards bodies and others blaming WG21 but all with somewhat fuzzy reasons. I’m curious if anyone has some info on the disagreements who isn’t actually deep enough in this to have taken a side already?
EDIT: Okay wow, so there’s P4334r0 which complains about contracts, a now-archived petition encouraging the DIS vote to fail, and P4433r0 (confusing numbering, much?) which argues that P4334r0 and the petition are incorrect. There’s a lotta history here, huh…
score 2 · canonical
My understanding is that Bjarne has been going around trying to prevent contracts from going in. I think he’s right on this one (even though I otherwise largely disagree with him wrt profiles), but it’s very hard for me to tell whether blocking the standard with the national bodies is remotely worth it or proportional.
No clue what happens next! I assume the ideal would be that contracts get thrown out, then they redo the vote and the standard passes, and hopefully this happens relatively quickly? Worst case would be that there’ll be no C++26?
score 1 · canonical
My understanding is that Bjarne has been going around trying to prevent contracts from going in. I think he’s right on this one (even though I otherwise largely disagree with him wrt profiles), but it’s very hard for me to tell whether blocking the standard with the national bodies is remotely worth it or proportional.
Oh wow, yes that seems quite severe. Looking more through some of these papers, I get some of the complaints for sure (mostly that relying on them for UB checks but then letting you turn them off is going to be a mess), but some of this wording seems like contracts are solely destructive. To be frank, the standards committees have been adding dysfunctional features for a long time, and sometimes they even later get fixed, so… I’m not sure if rounding up the international standards bodies here is a proportional action.
If Stroustrup is leading the fight against it, this does kinda seem more like a political fight, where some people who oppose it don’t really want to be overridden on anything (and, perhaps, some in support wishing for the opposite).
score 1 · canonical
There are multiple papers and afaik talks on “why contracts are bad” , I’d look them up for references. Afaik a lot of stuff about the one definition rule, and “how do you selectively enable or disable contracts” etc. I’d look them up for references if you want to dive deeper.
That said, afaik there was “strong consensus” to get contracts in by the standard bodies.
I have not fully kept up on the current technical statusof the draft but Bjarne being actively involved (and against contracts) is afaik confirmed.
score 2 · canonical
I would be very interested to watch those talks on why contracts are bad. Do you remember a name, the speaker, the conference or anything else which could be used to find them?
score 2 · canonical