[nanolith]

> You're missing some other critical components: the developers, and the costs.

No, I'm not.

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

> How many times more effort would it be...

I'd say compared to the 10% or so overhead of model checking, it would be approximately 8X as difficult, given that this requires learning a new language, using it correctly, and rebuilding the semantics in a way that is safe in that language. But, first, you need to learn new frameworks, rebuild all of the testing and quality assurance that went into the first development process, and rebuild the same level of trust as the original. Writing software is the easy part. It's all of the other stuff, like analysis, testing, confidence building, and engineering that costs money, and this would have to be redone from scratch, as the artifact from that original effort is being thrown away for a rewrite. Remember: the cost of rewriting software isn't just the cost of sitting down and banging out code.

> And how do the resulting turnaround times (say, compile/verification/etc. times) compare?

Model checking is actually pretty fast if you use proper shadowing. Compiling with C is lightning fast. I'd say that using a model checker is a little slower than compiling with Rust.

Also, you are mistaken that using a memory-safe language gives equivalent guarantees. It does not. A model checker allows you to write safer code. There are more errors than memory errors. Memory safety fixes many of the problems, but not nearly enough. So, after that rewrite, you'll also need to add a model checker or some other kind of formal methods to be as safe as just using the model checker to begin with. For Rust, that's Kani. It's not an apples to apples comparison.

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