Language workbenches

Context

This evaluates language engineering frameworks for building the compiler. The DSL needs entities, state declarations, operations with pre- and postconditions, invariants, and a type system; the compiler needs a parser, a type checker, IDE support over LSP, error reporting, and code generation (to OpenAPI, test harnesses, Z3 constraints, and so on). Four of the seven candidates are full language workbenches, integrated parser-plus-AST-plus-IDE frameworks, covered here; the lighter parser tools are on the next page.

Langium

Langium is an open-source language engineering framework written entirely in TypeScript by TypeFox, the creators of Xtext, and is the spiritual successor to it, designed from the ground up for the web and Node.js. It was at version 4.0 by mid-2025, with about 985 GitHub stars and roughly 254K weekly npm downloads across 82-plus dependent packages.

Its grammar language (.langium files) defines three things at once: the concrete syntax the user types, the abstract syntax tree (TypeScript interfaces, generated automatically), and the cross-references for name resolution. The grammar surface is rich:

• parser rules: Person: 'person' name=ID;
• assignments: = (single), += (array), ?= (boolean flag)
• cross-references resolved by name: person=[Person:ID]
• cardinalities: ? (optional), * (zero-or-more), + (one-or-more)
• alternatives with |, and unordered groups with &
• tree-rewriting actions for left-recursive expression patterns
• declarative infix operators (4.0) for precedence and associativity, parsing about 50% faster
• guard conditions (parameterized rules), data type rules, and reusable rule fragments

A grammar sketch for a service DSL:

grammar ServiceSpec

entry Specification:
    (entities+=Entity | services+=Service | invariants+=Invariant)*;

Entity:
    'entity' name=ID '{'
        (fields+=Field)*
    '}';

Field:
    name=ID ':' type=TypeRef;

TypeRef:
    primitive=PrimitiveType | reference=[Entity:QualifiedName]
    | collection=CollectionType;

CollectionType:
    kind=('List' | 'Set' | 'Map') '<' typeArgs+=TypeRef (',' typeArgs+=TypeRef)* '>';

PrimitiveType:
    name=('String' | 'Integer' | 'Boolean' | 'DateTime' | 'UUID');

Service:
    'service' name=ID '{'
        ('state' '{' (stateDecls+=StateDecl)* '}')?
        (operations+=Operation)*
    '}';

Operation:
    'operation' name=ID '(' (params+=Parameter (',' params+=Parameter)*)? ')'
    (':' returnType=TypeRef)?
    '{'
        ('requires' '{' preconditions+=Condition* '}')?
        ('ensures' '{' postconditions+=Condition* '}')?
    '}';

Invariant:
    'invariant' name=ID 'on' target=[Entity:QualifiedName]
    '{' expression=Expression '}';

infix BinaryExpr on PrimaryExpr:
    '&&' | '||'
    > '==' | '!=' | '<' | '>' | '<=' | '>='
    > '+' | '-'
    > '*' | '/';

What the grammar buys you, generated, is most of a language front end:

What it does not hand you is the type system. Langium ships no type-checking engine; the companion library Typir (typir-langium, also TypeFox) provides type inference, assignability checking, and validation hooks, but it is still maturing. Code generators are TypeScript functions you write to walk the AST, with traceability utilities provided, and Z3 has no built-in support but the official z3-solver WASM bindings drop into the same TypeScript project naturally. The project is an Eclipse Foundation project, used in production across several companies, and its Langium AI toolbox (2025) grounds LLMs on DSL knowledge with evaluation pipelines, boundary-respecting document splitting, and BNF-derived constrained decoding, directly relevant to the synthesis work. The learning curve is moderate: a TypeScript developer is productive within a week or two, and the grammar is intuitive for anyone who knows EBNF.

Xtext

Xtext is the mature predecessor, built on Java, Eclipse, and EMF, and the industry standard for DSL engineering since around 2010 (823 stars, Java 17+ and Eclipse 2024-03+). It and Langium line up closely:

For language development Eclipse is practically required: the grammar editor and generator run inside it, and although you can ship standalone language servers and CLIs, attempts to fully decouple from Equinox have stalled (the xtext.ide bundle still depends on org.eclipse.core.runtime). LSP is functional but retrofitted, LSP4J carries IDE-specific entanglements. The sharp weakness is large files: the CST consumes around 80% of memory, full workspace builds load every resource, EMF objects are not thread-safe (limiting parallelism), and files over 1MB can push response times past 1000ms. The recommendation is plain, do not pick Xtext for a new project in 2026: TypeFox themselves point new work at Langium, Xtext is in maintenance mode, and the only real draw, Xbase for a Java-like type system, is what Typir is filling in for Langium.

Spoofax

Spoofax is an academic language workbench from the Programming Languages group at TU Delft (163 stars on Spoofax 2, 14 on Spoofax 3), unusual in offering a declarative meta-language for every aspect of a language. There are three. SDF3 (Syntax Definition Formalism 3) is declarative syntax with disambiguation, layout sensitivity, error recovery, and scannerless parsing, which lets it compose languages without ambiguity. Statix, the most distinctive piece, is a constraint-based meta-language for static semantics built on scope graphs: you declare type rules as constraints over terms, name binding is modeled as a graph whose edges are containment, import, and inheritance, and name resolution and type checking happen in the same solver. It supports generics (shown with Featherweight Generic Java), structural records, and parametric polymorphism, and the specification is itself statically checked. Stratego, the third, is a term-rewriting language for transformation and code generation.

Statix is genuinely novel: rather than hand-code a type checker, you declare what the type system is and the solver does the checking, which for a DSL of entities, operations, contracts, and invariants reads very naturally.

typeOfExpr(s, FieldAccess(e, f)) = T :-
    typeOfExpr(s, e) == ENTITY(entityScope),
    resolveField(entityScope, f) == T.

Because the solver knows exactly which constraint failed, the error messages are excellent. The practical tradeoffs, though, are severe:

One notable industrial case study, OIL (Open Interaction Language) for control software, found Spoofax more productive than Python, especially for editor services, but that remains exceptional. The verdict: study Statix's scope-graph approach as intellectual inspiration for the type checker, but do not adopt Spoofax, the Eclipse-only IDE, missing LSP, tiny community, three-meta-language learning curve, and not-production-ready Spoofax 3 outweigh the elegance.

JetBrains MPS

MPS is a projectional editing environment (1,644 stars): instead of typing text that a parser turns into an AST, you edit the AST directly and MPS projects it as text, tables, diagrams, or mixed notations. The consequences are real, no parsing is required (the AST is the source of truth), languages compose without grammar conflicts, notations can include tables and math and widgets, and the editor permits only structurally valid edits so there are no syntax errors.

The catch is version control. Models are stored as XML, not human-readable text, so standard git diff and git merge are nearly useless on them; MPS ships custom UUID-based diff and merge tools, conflicts must be resolved inside MPS rather than any text editor or the GitHub UI, and code review on GitHub or GitLab is impractical because the XML diffs are unreadable. On scale, single-root elements handle up to about 4,000 lines comfortably and the tool has been tested on roughly 100,000 lines of C, with most users acclimating in a few days.

MPS is not suitable here. The DSL is text-based on purpose, to fit standard developer workflows, version control, code review, CI, and LLM generation, and the Git story alone is disqualifying. MPS shines for DSLs aimed at non-programmers who benefit from rich visual notations, which is not the audience here.