[synchronousq]

I just want to note, there exist two main flavors of formal methods: extrinsic techniques, which are disjoint from the code itself and generally reason about the specifications of code, and intrinsic techniques, which are inline with the code itself and reason about the code more directly. Historically, intrinsic techniques (such as type systems) reason about code at a functional level, while extrinsic techniques (such as decidable model checkers like Spin/P) reason about a model of the code, ascribed to formalism like an automata. But imo we're currently in a complete golden age of formal methods research, and extrinsic techniques are falling out of flavor in comparison to intrinsic methods as pushed by type system advancements and projects like Verus [1].

[1] https://github.com/verus-lang/verus

[adsharma]

TLA+ and the like work because they target a very small specification language.

With the large footprint of Rust, I've seen questions raised about how this will work. But haven't seen good answers.

Would love to read more.

[hashxyz]

I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.

[lolinder]

I prefer intrinsic techniques because it prevents the model from being out of sync with the implementation.

The thing that's never made any sense to me about using a marble checker for anything but concurrency issues (which are hard enough to warrant it) is that once you've validated your model you have to go actually implement it, and that's usually the most error prone part of the process.

If the correctness spec has to be written manually but prevents you from diverging from the spec in your implementation, that's a huge step up from extrinsic model checkers.