5 ms·

Not who you asked but I took a quick look. Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.

Not who you asked but I took a quick look. Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime. At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use. I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.

rramadass 3mo ago
Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++. See for example Can C++ be made as safe as SPARK? - https://www.eschertech.com/papers/index.php https://www.eschertech.com/papers/index.php which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.eschertech.com/2025/09/09/contracts-have-arrived-in-c/ https://critical.eschertech.com/2025/09/09/contracts-have-ar... Also see articles under Proving C and C++ programs correct - https://www.eschertech.com/articles/index.php https://www.eschertech.com/articles/index.php Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961 https://news.ycombinator.com/item?id=46298961

rramadass 3mo ago

Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++. See for example Can C++ be made as safe as SPARK? - https://www.eschertech.com/papers/index.php https://www.eschertech.com/papers/index.php which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.eschertech.com/2025/09/09/contracts-have-arrived-in-c/ https://critical.eschertech.com/2025/09/09/contracts-have-ar... Also see articles under Proving C and C++ programs correct - https://www.eschertech.com/articles/index.php https://www.eschertech.com/articles/index.php Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961 https://news.ycombinator.com/item?id=46298961