C++20 was supposed to have them, but they were removed on the very last minute, if we are lucky maybe C++23 will get them, but C++26 is most likely, if they ever go forward with them. [1]

For C you can have a look at Frama-C. [2]

D also has DbC. [3]

In case you can target Windows only, VC++ supports SAL Annotations, while not DbC they help to improve code security

[1] - http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p233...

[2] - https://frama-c.com/html/acsl.html

[3] - https://dlang.org/spec/contracts.html

[4] - https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-...

One thing I am excited about is that we should be able to exploit the contracts in some circumstances to better performance.

The problem I’ve seen with trying to add non-static contracts to performance-sensitive languages has been ideological rather than technical.

Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out).

But allowing them to be turned off in “release mode” eliminates much of the benefit in all modes: Developers can no longer assume that their code always runs in a context where the contractual guarantees are met, so they have to guard data integrity or safety critical operations dynamically anyway.

I guess it's as bounds check and other runtime validity checks integrated in the language. When we upgrade compiler versions, I usually run a global app profile (perf, and internal tools you must have when latency and cpu load are actual product requirements. Every 'new' hot spot is analyzed and if it's a contract, I check whether there's a less costly way to perform it, or if watering down the contract seems OK (usually not). The thing is, a precondition (especially if you went through AoRTE, or silver-level SPARK) can authorize you to aggressively remove all runtime checks (and get far more performant code) 'behind'.

> Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out).

Yes, with Ada it is typically a pragma or compiler-flag to turn checks off; however, Ada has a long history of having mandatory-checks and strongly-encouraging compiler-implementers to optimize the checks away when it is known they cannot fail (which is a surprising chunk of the time if you're coming from a C-based language).

They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs statically, eliminating the need for any checks.

I think the performance impacts are usually not as big as you think (the Ada compiler is smart enough to eliminate redundant checks where it can), and I believe that they can be turned off per package, too, so for performance critical modules they can be deactivated in release mode.

I do not think contracts were intended to raise recoverable errors in a normal application's behavior; if they are triggered, then the program is incorrect, not just encountering an error. I think most developers would leave them on in release mode (if possible) just to get stack traces and exception messages to see what failed.

The paper "Applying Design by Contract" by Bertrand Meyer shows how DbC is to be used. It is sufficient to have only preconditions turned on by default in "release" mode, others are optional.

My thumb rule is to have all preconditions/postconditions/invariants turned on only in the boundary functions (i.e. public api) of a module while the inner cohesive functions only have preconditions turned on.

Is it not possible to use refinement types to erase some (but maybe not all) runtime checks but still maintain a type safety guarantee?

Any language that has assertions can be used to simulate at least preconditions and postconditions, and maybe some support for invariants.

As the team leader for the second version of a database middleware product developed in C, being convinced by study of the efficacy of assertions for DbC and hence better quality software, I made sure my team used C assertions heavily throughout the codebase, at the entry and exit points of functions, to implement preconditions and postconditions, despite some opposition to it.

End result: the product was a success, and was used in multiple software projects for customers.

We were rewarded well for it.

Edit: I first learned about DbC myself, via reading about Eiffel and Bertrand Meyer's work, early on.

I should add that the product being a success wss not solely due to using assertions for DbC, of course, although, IMO, that did play a significant role in bug detection and hence removal and better product quality. I also ensured that the team consistently applied some other basic software engineering practices, which were not ordinarily followed in that company. The product success was the result of all the practices that were applied and also a good team.

I never understood how is that different from decorating your function with `assert` statements. Is it analyzed statically ?

Yes. SPARK/Ada will attempt to verify many of the properties statically. Not everything can be, and not everything can be done without significant effort (that is, more than it may be worth). But it's more than asserts in most other languages which are only verifiable dynamically. For those areas where SPARK can't prove something statically, the checks are used at runtime (like a traditional assert). It's a best of both worlds situation, in that regard.

asserts are just a language mechanism using which you implement preconditions/postconditions/invariants which are program correctness design constructs. Thus it is a systematic (i.e. not ad-hoc) way of using asserts correctly to guarantee program state.

I highly recommend reading Bertrand Meyer's papers "Applying Design By Contract" and "Design by Contract". They are well worth every programmer's time.

You can use formal verification tools to verify the code. Having preconditions ("assume" instead of "assert") reduces the search space.