alt Hacker NewsI can’t speak to the C++ contract design — it’s possible bad choices were made. But contracts in general are absolutely exactly what C++ needs for the next step of its evolution. Programming languages used for correct-by-design software (Ada, C++, Rust) need to enable deep integration with proof assistants to allow showing arbitrary properties statically instead of via testing, and contracts are /the/ key part of that — see e.g. Ada Spark.
Replies
The people who did contracts are aware of ada/spark and some have experience using it. Only time will tell if it works in c++ but they at least did all they could to give it a chance.
Note that this is not the end of contrats. This is a minimun viable start that they intend to add to but the missing parts are more complex.
Right, I think the tension here is that we would like contracts to exist in the language, but the current design isn't what it needs to be, and once it's standardized, it's extremely hard to fix.
> Programming languages used for correct-by-design software (Ada, C++, Rust) ...
A shoutout to Eiffel, the first "modern" (circa 1985) language to incorporate Design by Contract. Well done Bertrand Meyer!
The devil is in the details, because standardization work is all about details.
From my outside vantage point, there seems to be a few different camps about what is desired for contracts to even be. The conflict between those groups is why this feature has been contentious for... a decade now?
Some of the pushback against this form of contracts is from people who desire contracts, but don't think that this design is the one that they want.
But why? You can do everything contracts do in your own code, yes? Why make it a language feature? I'm not against growing the language, but I don't see the necessity of this specific feature having new syntax.
C++ is the last language I'd add to any list of languages used for correct-by-design - it's underspecified in terms of semantics with huge areas of UB and IB. Given its vast complexity - at every level from the pre-processor to template meta-programming and concepts, I simply can't imagine any formal denotational definition of the language ever being developed. And without a formal semantics for the language, you cannot even start to think about proof of correctness.