Haskell for non-Haskell's sake

[Peter Gammie]

Hal (and other interested parties):

I used Haskell to implement a model checker for a group of logics of time
and knowledge. In practice these are a bunch of extensions to the classic
CTL algorithms implemented in SMV [1].

The program itself (in terms of LOC) looks mostly like a compiler, and so
the standard arguments apply. However, Haskell is absolutely perfect for
implementing the SMV algorithms (and our variants) as they are cast in
terms of fixpoints of boolean functionals. Moreover performance isn't an
issue as a C library does the heavy lifting. (The program uses BDDs at the
moment.)

WRT Haskell, the only worry I had was that the program might leak space in
difficult-to-resolve ways, and the usual problem of BDD variable ordering
being difficult to control.

cheers
Peter.

[1] SMV itself is actually a LISP program written in C. (I think this is
self-evident from even a cursory glance, but the real giveaway is their
AST: who else, apart from a seasoned LISP hacker, would use CONS cells for
everything?)