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

[ad_hockey]

Lamport's rationale is that after an architect designs a building, the builders may still put electrical sockets in the wrong place and make other mistakes. But that's not a reason to start construction without a plan at all.

[lolinder]

That rationale assumes that writing software has a design stage and a build stage. It doesn't—software is the design, the building is done by the compiler or interpreter at runtime. So what's really being proposed is subdividing the design stage into a pre-design and a design.

Pre-design makes sense to me in certain limited circumstances. A limited amount of architecture planning can be valuable (though in most cases formal methods aren't useful for that), and for certain kinds of concurrent algorithms it could even be worth it to validate the design in a different language. But most of the time it's not worth doing the design twice when you can get pretty good guarantees from static analysis on the design (the code) itself.

[ad_hockey]

Agreed. To stretch the analogy, if I'm just replacing a fence panel or putting up a shelf then I'm not going to get an architect to create a blueprint. I'll know if it's right from the execution.

I sometimes work in areas where the error budget is essentially zero, with an element of concurrency, and for those there is a design stage before the build stage. I could see the value of formal methods there. At least I could execute a model with a model checker, which makes it one step closer to the code than a design doc or RFC.

Full disclosure: I haven't actually used formal methods myself, I've just been interested in the idea for a while and have done some reading on it.