Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property.
It is true that model checkers are much better are proving safety properties than liveness properties. I think it's not too far from the truth to say that model checkers are no good at proving liveness properties in real designs and that only safety properties work (somewhat well) in practice.
An alternative here is to abandon model checking altogether and focus on a powerful static analysis. I think the main challenge here is coming up with effective property specification schemes. A powerful type system like Haskell does in fact enable you to prove quite strong statements about your program. But you are inherently limited in terms of what you can prove to whatever it is that the type system can express. To me, it seems that model checkers allow more flexibility in specifying your property, especially when you take into account the fact that you can do your model checking on an augmented/instrumented version of your design.
> That's a different problem scale than "prove the whole thing works as specified".
On a vaguely related note, equivalence checking between designs, especially in the hardware context, is one thing that formal tools have had a lot of success with.
> you are inherently limited in terms of what you can prove to whatever it is that the type system can express
Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".
Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.
It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.
It is true that model checkers are much better are proving safety properties than liveness properties. I think it's not too far from the truth to say that model checkers are no good at proving liveness properties in real designs and that only safety properties work (somewhat well) in practice.
An alternative here is to abandon model checking altogether and focus on a powerful static analysis. I think the main challenge here is coming up with effective property specification schemes. A powerful type system like Haskell does in fact enable you to prove quite strong statements about your program. But you are inherently limited in terms of what you can prove to whatever it is that the type system can express. To me, it seems that model checkers allow more flexibility in specifying your property, especially when you take into account the fact that you can do your model checking on an augmented/instrumented version of your design.
> That's a different problem scale than "prove the whole thing works as specified".
On a vaguely related note, equivalence checking between designs, especially in the hardware context, is one thing that formal tools have had a lot of success with.