verlang

Verlang is a project seeking to enable formally-verified software development within the Erlang environment. It is currently highly experimental.

Background

Coq is an environment for functional programming with an integrated proof agent. The software development process with Coq is a bit non-standard: one doesn't ordinarily compile Coq source directly, but instead "extracts" the computationally-relevant portions to another language. Coq supports extraction to OCaml, Haskell, and Scheme, though at time of writing the OCaml target is the most mature.

Erlang is a functional programming language by Ericsson. Among Erlang's notable features is its support for hot-swapping of modules, enabling software updates with reduced downtime. To compile Erlang, one first converts it to Core Erlang, which is then compiled to a specific Erlang VM.

Verlang adds Core Erlang as an extraction target to Coq. From here it is possible to compile the extracted code and run it along-side ordinary Erlang modules.

Challenges

The theory behind Coq's extraction, as well as the majority of its present implementation, is due to Pierre Letouzey. His extraction mechanism is based on a two step process: first, Coq terms are translated into an internal language (MiniML); after that, target-specific code translates from MiniML into the target.

MiniML maps to Core Erlang in a more or less obvious manner, but as usual the devil's in the details:

• Core Erlang's notion of "modules" do not allow for nesting. Care must thus be taken when extracting MiniML into Core Erlang, as source in the former is likely to have nested modules.
• Core Erlang does not support currying. In fact, the (->) type constructor isn't even associative -- the arity of a function is encoded in its type, and a function of arity x which yields a function of arity y cannot be used as a function of arity (x+y).
• Core Erlang distinguishes between inner- and inter-module calls. The former are invoked with the apply construction, while the latter are invoked with call.
• Core Erlang's receive primitive is a special case of side-effecting case...of construction, for which there is no analog in MiniML. Thus one needs special trickery to provide "natural" access to this primitive from within Coq source.

There are other issues as well (dealing with Erlang's sum-type constructor |, for instance), but many of them can be managed through careful use of Coq's Extract command.

Status

Our work is highly experimental. We have a prototype extractor which attempts to address most of the challenges mentioned above:

• We support "module nesting" in a boring way: the outter-most module is preserved in the translation to Core Erlang, and name mangling is used to encode the sub-modules.
• We don't yet address problems related to currying. For the time being, we have been programming in Coq in such a way to avoid these issues in the extracted code.
• We treat all top-level function calls as inter-module calls, noting that a module is permitted to call into itself.
• We have admitted an axiom which describes receive (with finite timeout). The extractor recognizes a case...of around this axiom, which it translates into the desired Core Erlang.
• We don't (yet) generate Erlang header files for our modules (.hrl files).

It is currently possible to generate Core Erlang which fails with run-time exceptions (if you curry a function, for instance). We are still evolving the extraction theory, and thus there may be other bugs as well. Our goal is to resolve these issues and provide a rigorous implementation.

Example

The src/ideal_hash_tree path contains a model for Ideal Hash Trees in Coq. This model includes a setter and getter, with the property that the setter is guaranteed to return either (a) a new tree whose behavior under "get" is identical to the original, except at the key which has been set, or (b) another key, distinct from the one provided, whose hash collides with the hash of the given key.

This model is deficient in that it uses lambda abstractions instead of sparse arrays (we will move to sparse arrays Real Soon Now).

Noting that limitation, though, we are able to extract the model to Core Erlang, then compile and load the resulting module into the Erlang shell (erl). The src/ideal_hash_tree path shows the resulting Core Erlang file and contains instructions on how to experiment with the module.

Verlang-Coq

The pkg/aur path contains a PKGBUILD file for building Verlang-Coq as an Arch Linux package. This PKGBUILD is derived from the usual Coq respoitory in AUR, but it applies src/verlang.patch first, which adds Core Erlang as an extraction target.

For anyone performing a manual build, simply extract Coq (version 8.4pl2), apply the patch, then build and install as usual.

Future Releases

We are currently working on the next revision of the extraction facility, which will feature improved support for module extraction and bug fixes relating to the fname/variable dichotomy.