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.

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).

Related articles:

  • 2018-02-01 New OCaml library: path resolution
  • 2017-11-14 New OCaml parsing algorithm: tjr_simple_earley
  • 2017-09-17 Two new OCaml libraries: P0 and tjr-csv
  • 2017-09-06 ICFP most influential paper from 10 years ago
  • 2017-03-16 tjr-btree: a CoW B-tree library in OCaml
  • 2016-11-17 OCaml string functions
  • 2016-06-05 Do not buy TP-Link products
  • 2016-05-27 Visit to Cambridge, for REMS workshop
  • 2016-04-22 Visit to Denmark, to see Joergen Villadsen
  • 2016-02-19 Tree-structured text
  • 2016-02-09 Simple implementation of an Earley-like parsing algorithm
  • 2016-01-27 Talk at York University
  • 2016-01-06 Stephanie Heintz PhD viva
  • 2015-10-05 SibylFS presentation at SOSP'15
  • 2015-09-28 SibylFS SOSP poster
  • 2015-09-21 SibylFS presentation to Industrial Advisory Board
  • 2015-06-28 SOSP 2015 paper acceptance for SibylFS
  • 2015-06-26 P5 scala parsing library
  • 2015-04-21 REMS Cambridge talk on SibylFS
  • 2014-11-21 Talk on parsing at the University of Sussex
  • 2014-09-26 P1 combinator parsing library for OCaml
  • 2014-09-26 E3 earley parser library for OCaml
  • 2014-09-18 SLE 2014 conference, and Parsing at SLE workshop, slides
  • 2014-09-07 ICFP 2014, OCaml workshop, slides and video
  • 2014-09-07 ICFP 2014, Lem talk
  • 2014-07-11 P3 paper accepted for SLE 2014
  • 2014-07-11 Lem paper accepted to ICFP 2014
  • 2014-04-15 New release of P3 code on github
  • 2014-03-02 New release of P3 code on github
  • 2013-12-16 New release of P3 code on github
  • 2013-12-03 Implementing algorithms efficiently
  • 2013-11-24 Experience of using Lem
  • 2013-11-13 PhD student course on logic, proof and mechanized theorem proving
  • 2013-11-13 New website design
  • 2013-11-13 Engineer position
  • 2013-11-12 Netsem TCP/IP specification on github
  • 2013-11-08 Talk on parsing and P3 given at Cambridge
  • 2013-11-01 Funded PhD positions
  • 2013-04-01 PhD position funded by Microsoft Research
  • 2013-02-01 EPSRC grant funded
  • 2011-12-01 Verified parsing