14. Layered Strictness: Permissive DSL, Validating Emitter, Prescriptive Linter
Copy MarkdownDate: 2026-04-26
Status
Accepted
Context
TLX is a transpiler. The Elixir DSL is the input surface; TLA+/PlusCal is the output. The two languages have different idioms about what should be explicit:
- Elixir favors inference and convention. Spark DSLs amplify this — entity types are introspected, defaults are computed, atom values declare themselves as model values (ADR-0007). The "developer experience" default is "if it can be derived, derive it."
- TLA+ favors explicit declaration as a feature.
CONSTANTS,VARIABLES,EXTENDS, fairness assumptions — the explicitness is what makes specs auditable. A TLA+ practitioner reading a spec expects the parameterization to be visible at the top, not reverse-engineered from process bodies.
These idioms collide at the transpiler boundary. The concrete trigger was a discussion of CONSTANTS declarations: should TLX require users to declare them explicitly (TLA+ idiom) or auto-derive them from process parameters (Elixir DX, consistent with ADR-0007's atom handling)?
Three positions were considered:
- Mandatory explicit. Users must declare every constant, variable, and emitted symbol explicitly. Aligned with TLA+ tradition. Cost: a breaking DSL change requiring migration of every existing spec, with no benefit for users who just want to model-check a quick invariant.
- Mandatory implicit. Auto-derive everything that can be auto-derived. Aligned with Spark/Elixir DX. Cost: generated TLA+ becomes harder to audit for practitioners who care about the output, with no opt-in path to the stricter idiom.
- Layered. DSL permits both forms; emitter validates consistency when both are present; an external linter (the planned Credo plugin) recommends the explicit form for projects that want it.
The first two assume strictness is a binary global setting. The third recognizes that "strictness" has different correct answers for different audiences (throwaway specs vs. published reference specs) and locates each enforcement responsibility in the layer best suited to it.
Decision
TLX adopts a three-layer model for strictness decisions that cross the Elixir↔TLA+ boundary.
Layer 1 — DSL: permissive. The DSL accepts both implicit (auto-derived) and explicit (user-declared) forms wherever the choice is meaningful. Auto-derivation remains the default for low-friction Elixir DX, consistent with ADR-0007. Explicit forms are added as opt-in surface, never required.
Layer 2 — Emitter: validating. When both forms are present (a user-declared symbol and an auto-derived counterpart), the emitter validates that they agree. Disagreement is a compile-time error — the spec is lying about its parameterization, and that is a correctness invariant, not a stylistic preference. When only one form is present, the emitter behaves as today.
Layer 3 — Credo plugin: prescriptive. The TLX Credo plugin (covered in a separate ADR) provides opt-in checks that recommend the explicit form. Teams publishing reference specs alongside ADRs enable them; teams writing throwaway model-checking specs leave them off. Default off; users opt in via .credo.exs.
The generalizable principle behind this: explicit beats implicit when crossing language boundaries, but enforcement is a project policy, not a transpiler policy. TLX's job is to make both forms expressible and consistent. The decision of which form to require belongs to the project consuming TLX, not to TLX itself.
Scope boundary. This ADR codifies the pattern. It does not introduce explicit forms for any specific symbol class; those land as separate work, each with their own DSL surface decision and Credo check. ADR-0007 (auto-declared atom model values) continues unchanged — it remains the default behavior under Layer 1.
Consequences
Positive:
- No breaking changes. Existing specs (
examples/forge/, downstream consumers) keep working. - Adoption becomes a per-project, per-team decision rather than a coordinated migration.
- Future strictness questions ("should X be explicit?") have a recorded principle to apply rather than re-deriving the argument case-by-case.
- Aligns with how Credo itself is organized: the language allows things, the linter recommends or forbids them.
- The emitter's consistency check catches a real bug class (declared symbol disagrees with derived symbol) that neither pure-implicit nor pure-explicit designs catch.
Negative:
- Three layers to maintain. Each new symbol class that gains an explicit form needs (a) DSL surface, (b) emitter consistency rule, (c) optional Credo check.
- Documentation cost: the existence of two valid forms must be explained, with guidance on when each is appropriate.
- The Credo plugin becomes a non-trivial component to keep version-locked with TLX internals, since checks reference DSL state and emitter derivation logic.