Relevance of model checking in strongly typed functional programming languages?

10
votes

I am currently learning about model checking (modal logic, LTL, CTL, SAL model checker, etc.) and in my spare time I am learning about Idris which is a strongly typed functional programming language that supports dependent types. Since I am looking at both model checking and Idris, I start to get curious about how Idris relates to Formal Methods and model checking.

When learning about model checking, it feels like most examples brought up is either about verifying systems written in an imperative manner or hardware components. So I am puzzled about the relevance of model checking in strongly typed functional programming languages and especially in a dependently typed language such as Idris where it seems to me that the type checker already does a fantastic job at verifying correctness. My intuition, however, tells me that model checking maybe is relevant for partial functions that doesn't give any promises of termination.

Is model checking relevant when using a strongly and dependent typed programming language such as Idris?

1
idrismodel-checking

1 Answers

4
votes

You are right that model checking is most often used for hardware verification and imperative (often concurrent) programs, since its origin is also in this area. For functional programs, elaborate type systems techniques are widely used for verification. However, they often require a lot of annotations, or might produce "false positives", resulting in refuting a "correct" program. Model checking does not require these annotations, and can also allow more specific questions to be answered. I am not an expert in the field, but it seems that techniques from type systems and model checking are often combined for functional programs. If you are interested in current research and approaches for Model Checking of functional programs, there is an excellent course with lots of material online:

http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13

The course has been prepared by Luke Ong, one of the leading researchers in the field.