Hardware design languages have been continuously increasing their abstraction levels over the last 20 years, and languages such as very high speed integrated circuit hardware description language (VHDL) and Verilog have become standards in the field. These languages lack a formal basis, however, which is needed, for instance, to formally verify designed circuits.

Nowadays, Haskell (see http://www.haskell.org) is the most important pure functional language. Its strong mathematical foundation (it is based on lambda calculus) makes it a very convenient language to perform formal verification of programs.

In this work, the authors describe the hardware design language, Lava, that has been embedded into Haskell. The authors describe how Lava takes advantage of many features of Haskell, such as monads or type classes, to completely describe hardware circuits, and how many existing tools, such as theorem provers (which allow users to perform formal verification of circuits), can be used with Lava.

The paper is well written, and clearly explains the advantages and properties of Lava using many examples. Although some related work is described, the authors only mention a short comment about Hawk [1], another language embedded in Haskell, which uses a very similar approach to hardware specification. A more detailed comparison between them would have been very interesting.

Finally, Lava has become the core of Claessen’s Ph.D. thesis [2], so I refer the interested reader to this document for a more detailed explanation about Lava.