[nanolith]

The reason why so few developers use model checking tools is because there is limited documentation out there for how to use them effectively. That is changing. Hell, I'm writing a book on the subject.

These tools aren't difficult to use. They just aren't well documented.

I've got better things to do with my afternoon than model check random bits of code in a forum. You wouldn't ask someone talking about a unit testing framework to unit test an example that you write up. If you're curious, I'm writing a book on model checking C, which will be going off to the publisher sometime in 2025. There are also examples online.

[dataflow]

> I've got better things to do with my afternoon than model check random bits of code in a forum. You wouldn't ask someone talking about a unit testing framework to unit test an example that you write up.

I totally would, and I would also reply to their example. I've exchanged code examples in the past right here on HN for discussions like this.

You obviously don't have to do anything, but if you're going to claim it's only a 10% difference compared to unit testing -- expect people to be skeptical unless you can show side-by-side examples.

> If you're curious, I'm writing a book on model checking C, which will be going off to the publisher sometime in 2025. There are also examples online.

I'm not at all curious about model checking C. I've seen that before numerous times, and frankly, even if you could cut the development cost in C by 50% through model checking, I still wouldn't be interested.

You keep going back to C... in a conversation that's that's supposed to cover C++. I'm not sure why you do this, if the solutions to them are actually comparable -- a lot of the world is on C++, so you would find a much, much broader audience if you cater to that. My suggestion (and you're obviously welcome to ignore me, but I'm just letting you know my reaction as a reader) is to focus your response letter & book at least partly on visibly demonstrating how your proposed solutions would have similar success on C++. If you don't sell people on this being a solution for C++, I doubt your writing will make many people change their minds about switching to a different language.

[nanolith]

I'm focused on C because a lot of our critical infrastructure is written in C. The Linux / BSD kernels, firmware, etc. It's also where my interest is. Model checked C is a good enough balance of cognitive load, safety, and time to market for my purposes. Others may disagree.

Tooling exists in C++. That shouldn't be too surprising given that the C++ abstract machine model is not much more complex than C and has similar complexities as Rust. The same techniques work there as well. If someone wants to tap that audience by translating this process to C++, they are welcome to do so.

[whytevuhuni]

What are some of the tools you'd recommend?

In my case I'm working with Nginx and I'd like to make a few custom modules safer.

[nanolith]

For C, I recommend CBMC.