The Problem Nobody Solves Completely
Every software system has business rules. An account balance cannot go negative. An order must be fulfilled within 24 hours. A user flagged for review cannot simultaneously be marked as cleared. These constraints are the semantic backbone of any application — and every programming language handles them differently.
We recently conducted a systematic comparison of three language ecosystems — Gleam, Elixir, and Lua — to understand how each approaches the problem of making invalid states unrepresentable. The findings illuminate a gap that none of them fill.
Three Philosophies, Three Trade-Offs
Gleam: Prevent It at Compile Time
Gleam is a statically typed language running on the BEAM virtual machine. It uses algebraic data types and opaque types with smart constructors to make invalid states literally unrepresentable in the type system. If the code compiles, the constraint holds. There are no null values, no implicit conversions, and no exceptions — only explicit Result types for error handling.
The limitation is rigidity. Type-level constraints are static. You cannot reconfigure them at runtime, express temporal properties (“this must become true within 24 hours”), or describe transformation constraints (“the total balance before and after a transfer must be conserved”). The type system encodes what states can exist, but not how states may change over time.
Elixir: Validate at Boundaries, Trust Internally
Elixir takes a layered approach. Its Ecto changeset pattern is particularly instructive: a pipeline of validations applied to data before it enters the database — field-level checks, cross-field constraints, format validations, and custom business rules, all composed declaratively. This is the closest any mainstream framework comes to separating “what must be true” from “how the system operates.”
Elixir’s philosophy is pragmatic: validate at system boundaries, trust internal code, and if something unexpected happens, let the process crash and restart cleanly. This works well for concurrent systems but means business rules are scattered across changesets, guard clauses, GenServer callbacks, and pattern matches — there is no single artifact that captures “all the rules.”
Lua: Maximum Flexibility, Minimum Guarantees
Lua occupies the opposite end of the spectrum. A minimal, embeddable scripting language (∼200KB runtime) designed to be hosted inside other systems. Business rules are expressed as explicit runtime checks: assertions, type guards, conditional logic. Typed variants like Luau add gradual typing, but even these provide limited constraint expression compared to Gleam or Elixir.
The Gap: Where All Three Fall Short
| Capability | Gleam | Elixir | Lua |
|---|---|---|---|
| Named, reusable constraints as first-class entities | No | No | No |
| Temporal logic (“must become true within N hours”) | No | No | No |
| Transformation validation (before/after state) | No | No | No |
| Part-whole relationship tracking | No | No | No |
| Semantic types with domain meaning | No | No | No |
| Bidirectional violation tracing | No | Partial | No |
Gleam encodes constraints in types — powerful but static. Elixir distributes constraints across multiple runtime layers — flexible but fragmented. Lua leaves constraints to the developer — simple but unenforceable.
What is missing is a unified, declarative specification of semantic constraints that is separate from implementation, formally verifiable, temporally aware, and language-agnostic.
Constraints as a Formal Calculus
The gap these three ecosystems reveal points to a different kind of artifact — one where entities, predicates, and invariants are first-class constructs, not annotations on application code, but independent semantic artifacts compiled and enforced by a dedicated runtime.
The core abstraction is the entity-predicate-invariant triad: an entity defines what exists in the domain; a predicate defines what must be true; an invariant binds a predicate to an entity type, enforced on every state change.
This diverges fundamentally from type-system approaches in two areas. Transformation predicates validate state transitions — ensuring, for example, that the total balance is conserved across a financial transfer. Temporal invariants express time-bound properties — “this order must be shipped within 24 hours.” No type system can express these. No changeset pipeline tracks whether a state transition is valid given the full history.
What Each Language Teaches
From Gleam: The principle that invalid states should be structurally unrepresentable. Some constraints could be provable at compile time rather than enforced at runtime. Gleam’s multi-target compilation (BEAM and JavaScript) also suggests that semantic schemas could generate type definitions for multiple host languages.
From Elixir: The layered validation model. Not all constraints carry equal enforcement cost. A formal constraint language could benefit from constraint weighting — some predicates as cheap guards, others as full validations. Elixir’s OTP supervision model also suggests that constraint violation should trigger structured recovery, not just rejection.
From Lua: The embeddability imperative. A semantic constraint engine that can only run as a standalone system has limited adoption surface. A minimal runtime designed for embedding could bring semantic constraint enforcement to systems that currently have none.
The Strategic Opportunity
The most significant insight is architectural. A formal semantic constraint layer does not compete with Elixir, Gleam, or Lua. It occupies a different layer in the stack — above the application code, below the business requirements.
A semantic schema could serve as the formal specification for a Gleam application’s domain invariants, an Elixir GenServer’s state machine, a Lua-embedded system’s constraint checks, or a TypeScript API’s validation layer. One schema, multiple generated enforcement surfaces.
Type systems prevent some invalid states. Runtime validation catches others. Explicit checks handle what remains. But none of these mechanisms provide a unified, declarative, temporally aware specification of what must be true about a system’s state and state transitions. The evidence from Gleam, Elixir, and Lua suggests the industry needs exactly that — a formal specification language for semantic constraints that generates enforcement for all of these platforms.