While I can understand that C++ contracts were met with controversy, contract annotations scoped at analysis time that can be verified by external tools, such as static analyzers, model checkers, or automatic theorem provers, are incredibly useful.

I put together an alternative function contract and invariant mechanism in C using CBMC and custom macros that effectively allows me to perform formal methods in C using compositional verification. The reason why I chose C is because of its relative simplicity and relative ease of building tooling around it. C++ contracts provide some feature parity, and would let me take advantage of some of the features in C++ relative to C.

I hope that the contract proposal is workshopped and simplified so it can be proposed again for a future version. Its current form is unsuitable, but it deserves a second chance with a simpler implementation. Contracts would narrow the safety gap between C++ and languages such as Ada / SPARK.