3 ms·

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

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.

vlovich123 2y ago
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.
- nanolith 2y ago
  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.
  - vlovich123 2y ago
    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.
    - nanolith 2y ago
      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.

vlovich123 2y ago

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.

nanolith 2y ago
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.
- vlovich123 2y ago
  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.
  - nanolith 2y ago
    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.