Top all-time · #25568
David Crocker
Personal blog · critical.eschertech.comprogrammingsystems
David Crocker's personal blog at critical.eschertech.com covers programming and systems. Since 2014, 3 different Hacker News readers have linked it 4 times. It is still writing: the last post was on 2025-09-09, and you can follow it by feed.
Too few sampled comments (3) to say how often HN recommends it.?
Why HN links it
HN readers link David Crocker's verification blog for its writing on formal verification of C code and design-by-contract, including concrete examples and contracts in C++.
Summarised by Claude from a sample of 3 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Formal verification of C/C++ code for critical systems
What Hacker News says?
Here [0] is a concrete example of using a formal verification system ontop of C (and the blog contains many other examples) along with an excellent dialog around the example. First a caveat, this formal verification system is rather simple, and only proves code within the domain of the C standard. Using such a system with a buggy C compiler (pretty much all of them) or the result on subtly incorrect hardware (like m…
Comment linking /2010/06/22/aliasing-and-how-to-control-it/
on “Hacker-Proof Code Confirmed”Submitted Danger – unsigned types used here (2010) as a story · 1 points
HN discussionWhich 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 which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.es…
Comment linking /2025/09/09/contracts-have-arrived-in-c/
on “Formal Methods and the Future of Programming”Have you looked at "Verified Design-By-Contract"? See the paper Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm by David Crocker here - https://www.eschertech.com/products/verified_dbc.php David Crocker's Verification Blog - https://critical.eschertech.com/
Comment linking /
on “Formal Methods and the Future of Programming”