Syntax and Semantics 2: Three ways to define what your code means

The previous post defined syntax: the set of things you are allowed to write. ADTs define a grammar. Pattern matching destructures it. But none of that answers the real question: what does the code mean?

That question has a name. It is called semantics. And there are exactly three formal ways to answer it.

These three approaches were developed independently by different researchers between the late 1960s and early 1980s. The remarkable thing is not that they exist; it is that working programmers use all three daily without ever learning their names.

Operational semantics: match as reduction rules

#

Origin: Gordon Plotkin (1981), building on Robin Milner’s earlier work. The idea is simple: define the meaning of a program by describing how it executes, step by step, one reduction at a time.

If you have ever written a match expression that evaluates an expression tree, you have written operational semantics. Each match arm is a reduction rule. Each recursive call is a step. The formal notation looks like this:

────────────────── (E-Num)
Num(n) => n

     e1 => v1    e2 => v2    v3 = v1 + v2
──────────────────────────────────────────── (E-Add)
             Add(e1, e2) => v3

Now look at the code. In Rust:

fn eval(expr: &Expr) -> f64 {
    match expr {
        Expr::Num(n) => *n,                       // E-Num
        Expr::Add(l, r) => eval(l) + eval(r),     // E-Add
        Expr::Mul(l, r) => eval(l) * eval(r),     // E-Mul
    }
}

In Scala:

def eval(expr: Expr): Double = expr match {
  case Num(n)      => n                    // E-Num
  case Add(l, r)   => eval(l) + eval(r)    // E-Add
  case Mul(l, r)   => eval(l) * eval(r)    // E-Mul
}

These are not analogies. Each match arm is literally a reduction rule translated from mathematical notation into executable code. The comments are not decorative; they are direct references to the formal rules above.

There is a bonus. Both Rust and Scala require exhaustive matching. If you add a new variant to the Expr enum and forget to handle it, the compiler rejects your code. This is totality checking: the compiler is proving that your operational semantics is defined for every possible input. Not most inputs. All of them.

Denotational semantics: functions as mathematical objects

#

Origin: Dana Scott and Christopher Strachey (late 1960s-70s). Instead of describing how a program executes, denotational semantics describes what a program denotes: a value in a mathematical domain.

The core insight is disarmingly simple: a pure function is a mathematical mapping. The function fn add(x: i64, y: i64) -> i64 does not merely compute addition; it denotes the mathematical function + over integers. No side effects, no hidden state, no difference between the program and its meaning.

This gets interesting with type classes. A trait implementation defines what abstract operations mean for a concrete type. When you write a Monoid instance, you are providing a denotation: a specific mathematical interpretation of empty and combine:

trait Monoid {
    fn empty() -> Self;
    fn combine(self, other: Self) -> Self;
}

impl Monoid for i64 {
    fn empty() -> i64 { 0 }
    fn combine(self, other: i64) -> i64 { self + other }
}
// This IS a denotation: ⟦i64 under Monoid⟧ = (0, +)

trait Monoid[A] {
  def empty: A
  def combine(x: A, y: A): A
}

given Monoid[Long] with {
  def empty = 0L
  def combine(x: Long, y: Long) = x + y
}
// This IS a denotation: ⟦Long under Monoid⟧ = (0, +)

The double-bracket notation ⟦...⟧ is standard in denotational semantics. It means “the meaning of.” When you write impl Monoid for i64, you are saying: the meaning of i64 under the Monoid interpretation is the algebraic structure (0, +). Change the implementation and you change the denotation. Same syntax, different semantics.

Scala takes this further. A for-comprehension is denotational semantics for effectful sequencing. for { a <- getUser; b <- getOrders(a) } yield b denotes the composition of two effectful computations in a monadic context. The syntax describes the shape; the Monad instance provides the meaning.

Rust has its own version. The From and Into traits define semantic morphisms: meaning-preserving transformations between types. impl From<String> for UserId says: there exists a well-defined mapping from strings to user identifiers. The conversion is not accidental; it is a declared semantic relationship.

Axiomatic semantics: invariants enforced by the compiler

#

Origin: Tony Hoare (1969), building on Robert Floyd (1967). The idea: define meaning not by execution or denotation, but by what is guaranteed to be true before, during, and after a piece of code runs. This is Hoare logic: {P} C {Q}: if precondition P holds before command C, then postcondition Q holds after.

Rust’s entire ownership model is axiomatic semantics.

The borrow checker enforces preconditions (you cannot have aliased mutable references), postconditions (allocated resources are freed when ownership ends), and invariants (data is valid for its declared type, always). You never write these axioms explicitly. The compiler knows them.

But you can encode custom axioms in the type system. Consider NonZeroU32:

// Axiomatic: NonZeroU32 encodes the precondition IN THE TYPE
fn divide(n: u32, d: std::num::NonZeroU32) -> u32 {
    n / d.get()  // No runtime check needed -- the invariant is axiomatic
}

The precondition “divisor is not zero” is not a comment, not a runtime check, not a hope. It is a type. The caller must prove the precondition by constructing a NonZeroU32, which can only be created from a verified nonzero value. The axiom is enforced before the function is ever called.

The type-state pattern pushes this further, encoding state machine invariants at compile time:

struct Door<State> { _state: std::marker::PhantomData<State> }
struct Locked;
struct Unlocked;

impl Door<Locked> {
    fn unlock(self) -> Door<Unlocked> { /* ... */ }
}

impl Door<Unlocked> {
    fn open(&self) { /* ... */ }
    // Cannot call open() on Door<Locked> -- the compiler enforces the axiom
}

You cannot call open() on a locked door. Not because of a runtime check. Because the type system makes it syntactically impossible. The axiom “only unlocked doors can be opened” is encoded in the type parameter, and the compiler rejects any program that violates it.

Scala approaches this differently. Where Rust encodes axioms structurally, Scala offers explicit Hoare-style contracts via require and ensuring:

def divide(n: Long, d: Long): Long = {
  require(d != 0, "divisor must be nonzero")  // Precondition
  n / d
} ensuring { result =>                         // Postcondition
  result * d + (n % d) == n
}

Different mechanism, same formal framework. Rust enforces axioms at compile time through types. Scala states them explicitly as runtime contracts. Both are axiomatic semantics.

The bridge: pattern matching as the interpretation function

#

These three approaches might seem separate, but they converge in one place: pattern matching.

An ADT defines the grammar: what shapes exist. The match arms define the semantics: what each shape means. Together, the match expression IS the interpretation function: the formal bridge from syntax to semantics, written ⟦.⟧ : Syntax -> Semantics.

Here it is, made explicit:

Interpretation function ⟦.⟧:
  ⟦Num(n)⟧    = n              (syntax -> value)
  ⟦Add(l,r)⟧  = ⟦l⟧ + ⟦r⟧     (compositional)
  ⟦Mul(l,r)⟧  = ⟦l⟧ * ⟦r⟧

Every eval function you write for an expression tree is this function. The Expr enum is your syntax. The match body is your semantics. The function signature fn eval(expr: &Expr) -> f64 is the interpretation function’s type signature. You have been writing formal semantics the entire time.

Here is how all the constructs map:

What comes next

#

These three frameworks are not mutually exclusive. A single codebase uses all three simultaneously. Your match is operational. Your pure functions are denotational. Your type constraints are axiomatic. The language does not force you to choose; it layers them.

But there is a tension hiding inside this layering. When you want to add a new variant to your enum and a new operation over it, one of these approaches has to give. That tension has a name, and the next post examines it: the Expression Problem.