Another related language is Maude. It's a term-rewriting language, so for example we can implement arithmetic by defining symbols to represent numerals (eg. "ze

Another related language is Maude. It's a term-rewriting language, so for example we can implement arithmetic by defining symbols to represent numerals (eg. "zero" and "successor") and some rewrite rules which implement addition, subtraction, multiplication, etc. This is similar to languages like Pure, which lets us write code in a pure-functional style, but with the bonus that rewriting can avoid awkward recursion schemes (eg. "a + b" can recurse on both arguments at once). This makes it well-suited to implementing domain-specific languages. However, Maude can go further than other rewrite languages since it is also a model checker: if A rewrites to B, we can supply A and get back B; or we can supply B and have Maude search for an A. If A and B are DSL terms, we can derive terms from their properties, as is being discussed here. We can also have Maude show that some terms are unreachable, for example that there is no input which rewrites to an Error symbol. Of course the advantage to Z3 is that it's hooked up to fast domain-specific solvers (SAT, SMT, arithmetic, etc.), whilst Maude's search is general-purpose and therefore slower.