Domain specific languages (DSL) can be well suited for certain business scenarios and be easier to learn for non-developers. We present our experience using the Coq proof assistant to support the formal specification and the compilation for three different DSLs: JRules (a language for business rules), SQL (a language for relational databases), and Jura (a language for legal contract).

We describe how each of those languages comes with its own challenges, and how they benefit differently from the use of a proof assistant. We also show how we could exploit their commonalities to build an optimizing and (partially) verified compiler for each of them. The core of that compiler uses traditional database representations (the Nested Relational Algebra and its corresponding Calculus) for optimization and code-generation.

– Some of this work was done jointly with Joshua Auerbach, Martin Hirzel, Louis Mandel and Avi Shinnar as part of the Q*cert project (https://querycert.github.io/).