[dataflow]

>> If you come up with processes and tooling that is difficult to use widely,

> That's an unfounded assumption. The tooling and processes I have developed are no more difficult to use than unit testing.

My assumption was just founded on the reality of how few developers use model-checking tools, and how they difficult they find them. If your tools are radically better, and they work for C++, that's obviously amazing.

Could you give us an idea of what the equivalent of this simple C++ code would look like, so we can see how it looks in comparison? You know, with whatever bells and whistles you need to add to it for the model checker to verify its correctness:

  #include <string>
  #include <unordered_map>
  
  template<class Char>
  auto make_map(size_t argc, const Char *const argv[]) {
    using S = std::basic_string<Char>;
    std::unordered_map<S, S> map;
    for (size_t i = 0; i + 2 <= argc; i += 2) {
      map[S(argv[i])] = S(argv[i + 1]);
    }
    return map;
  }
  
  int process(const std::unordered_map<std::string, std::string> &);
  
  int main(int argc, char *argv[]) {
    return process(make_map(argc, argv));
  }

[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.