Date: 2013-11-24
Categories: lem; news; software

Experience of using Lem

Recently I had occasion to use Lem. Lem is a specification tool. To a first approximation, it provides the ability to specify systems using a syntax similar to OCaml, but with added capabilities to handle logical constructs. I ported the Netsem TCP/IP specification from HOL to Lem. The following are my thoughts.

Currently, when writing a formal specification, one chooses a theorem prover such as HOL, Isabelle or Coq, and one starts to write using that particular tool. The resulting specification usually never escapes the initial tool. Lem offers the possibility of a single source specification which is then translated to the different dialects used by the main theorem provers.

Why would you want a specification to be usable in another tool? Many possible reasons.

typically you want to use tool features that are not present in your initial tool
or you want others to work on the specification (but they do not want to learn your initial tool)
or you want to prove some results in a particular theorem prover (because the libraries are better, or something)
or perhaps your initial tool is dying, and you really value the specification, and want to preserve it by making it available to other provers

Assuming you want your spec to be available in other tools, you don't have to use Lem. For example, if your spec is small, just rewrite it in the other tool. This gets costly if the initial spec keeps changing, or is not so small. It is also costly if you want to support many different provers. At this point, people usually resort to writing a parser for the language of their initial tool, and a pretty-printer for the new tool. For example, I have quite a few tools (most unmaintained) called things like "ocaml-to-isabelle", "ocaml-to-hol", "isabelle-to-hol" etc. This is all quite painful.

Lem offers an alternative. The syntax of Lem is similar in many ways to that of HOL, Isabelle and OCaml (I don't know Coq so well, but maybe it is also similar to Coq). You write the specification once in Lem, and then Lem will generate different versions of the specification in the different tools. This is extremely useful.

Lem is also a reasonably pleasant tool to use to write a specification. Although it doesn't have an interactive REPL, it is amazingly fast to process Lem specifications. For example, the Netsem TCP/IP spec is processed by Lem in a few seconds or so (essentially this involves parsing and type-checking the specification). It takes HOL much longer to process the HOL version of the spec. Of course, Lem is doing a lot less than HOL, but for the most part, when developing a spec, one wants a rapid turn around. When the spec has settled, then one can wait for HOL to dot the "i"s and cross the "t"s.

Lem also has some nice features such as type-classes. However, the main benefits of Lem are surely that it allows a specification to be ported easily to other theorem provers, and that it can process specifications relatively quickly when compared to existing tools such as HOL. I intend to use Lem for my next few specifications (including the filesystem spec that I am currently working on).