Comment by nanolith | Hacker News Reader

Comment by nanolith | Hacker News Reader

In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and others.

I consider bounded model checking to be "formal methods lite". It provides most of the benefits at a lower cost of entry than using a proof assistant or building constructive proofs. Really, there's little added overhead. Perhaps 30% to 40% more time to build out the function contracts and model checking. Given that this overhead more or less prevents errors that would likely be introduced without it, I think it's a reasonable investment.

TLA+ is certainly related, since it uses an SMT solver at its base. I see it as useful for designing algorithms and protocols. A tool like CBMC or Kani provides similar guarantees at the source code level. It's not perfect, as currently CProver does not have direct threading support, but with a reasonable application of method shadowing and function contracts, even things like threading can be anticipated. Using a bounded model checker effectively means changing the design of software to work best with it. This is little different than using concepts like TDD or continuous integration.

In my experience traditional property checks are pretty difficult to write already (30-40%). I get the sense that a bounded model check would be even more expensive than that, probably into the 2-3x range if not more. I’m talking about meaningfully complex logic, not very simple things.

It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy to write, when your property aligns well with property checking models! But then time-based stuff like TLA+ ends up working way better, sometimes.

There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.

You can write these checks as assertions in your regular source language. It's no more difficult than writing runtime parameter checks, really.

There are some complexities, to be fair, but these are mostly around the performance of the model checker. Some things are easy to check, and other things, like loops and recursion, are harder to check. However, this is a matter of optimization, and with practice, this becomes quite easy to deal with.

As I said I use property checks as much as possible, but they’re still cumbersome and the complexity and difficulty scale non-linearly with the complexity of the interface; some properties are easy to write whereas others are so difficult I can’t imagine how to write a generic property for all situation vs resorting to boundary conditions I think of. The challenges with the model checker is that there’s all sorts of constructs it can’t test. For example, Kani can’t handle await expressions which is a huge obstacle for any async Rust code.

Threading and async are an issue with the current CProver core. But, much of that can be simulated by writing helper functions that get shadowed during the model checking.

It's simply not possible to make a bounded model checker work on arbitrary code, so instead, the code should be factored to work within the constraints of the model checker. The result is safer code, even if the style is different.

I never said threading. I use a single-threaded runtime. But the lack of any async support even though it’s basically syntactic sugar at that point makes it a non-starter. There’s some amount of “make your code testable” that’s valid, but completely rewrite how your application is written and thus you can’t use the frameworks you need to is a bit much. At some point the testing framework has to also meet you where you are.

kani certainly could be extended to have better async / await support. But, I think this is a larger engineering problem. The value of code that has been verified using an existing model checking tool is greater than the value of code using a particular framework and hoping that Some Day there will exist a tool that will work with that framework.

I'd wrap libraries that were problematic to build function contracts around before I punted on model checking. Hell, I'd fork and refactor these APIs to work with lightweight fibers before I gave up on model checking. The utility of something like async / await is small potatoes compared to the utility of having code that has even light formal verification in place.

In Java it would be something like JBMC?

Yep. JBMC is part of the CProver / CBMC family.

Reply on news.ycombinator.com