>> I think it is a pragmatic way of producing code that can approach the robustness of formal verification in practice with a lot less work, so the ROI is high.

>> I think it is a pragmatic way of producing code that can approach the robustness of formal verification in practice with a lot less work, so the ROI is high. This is correct. Design by Contract techniques help to ensure that code is robust and works as expected. It is good that C++ is getting these tools through compiler plug-ins. The Ada programming language added support for Design by Contract in Ada 2005: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... The same language syntax used to define preconditions, postconditions, and invariants in Ada paved the way for SPARK to prove program correctness: https://learn.adacore.com/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.html#contracts https://learn.adacore.com/courses/intro-to-spark/chapters/03... Hopefully Design by Contract can be included in the C++ standard itself in the future.