What a Formal Semantics Is

Here is a one-line program. What does it mean?

x = 1; y = x + x; x = y * y

You probably answered instantly: x ends up 4. But how did you know? You ran a little machine in your head — a machine whose rules you were never formally told, and which the language designer never wrote down in one authoritative place. For a toy like this the informal picture is fine. For a real language — where a[i++] = i has a different result in C than your intuition suggests, where "evaluate the operands left to right" was for decades unspecified and compilers disagreed — informal meaning is a disaster. A formal semantics is the cure: a precise, mathematical answer to the question "what does this program mean?", stated so exactly that two people (or two compilers) can never legitimately disagree.

This is the founding question of programming-language theory. A grammar tells you which strings are well-formed programs — but says nothing about what they do. Semantics supplies the missing half: a mathematical object (a value, a state, a function, a relation) that is the meaning, together with rules that compute it. Get this right and you can prove things: that an optimisation preserves behaviour, that a type system rules out crashes, that two programs are interchangeable. Everything else in this course is built on it.

Object language vs metalanguage

The first discipline a semanticist learns is to keep two languages rigidly apart. The object language is the one we are studying — the programming language whose meaning we want to pin down. The metalanguage is the one we reason in — ordinary mathematics: sets, functions, relations, inductive definitions, logic. Confusing the two is the classic beginner's error; it is the sin of thinking the symbol + inside a program and the addition operation + on the integers \mathbb{Z} are the same thing. They are not: one is a piece of syntax, a mark on the page; the other is a mathematical function that the semantics uses to explain the mark.

Object language. The syntax under study. Its expressions are inert data — trees of symbols with no inherent meaning until the semantics assigns one.
Metalanguage. The mathematics we use to talk about the object language. When we write \llbracket e \rrbracket = 4, the brackets \llbracket \cdot \rrbracket quote an object-language expression and the 4 on the right lives in the metalanguage.

We even use a distinct arrow style for each world. Object-language operators (+, *) are typeset as program text; the metalanguage's genuine operations are ordinary maths. Whenever an object symbol and a meta operation share a glyph, we lean on context — or decorate one — to keep the border patrolled. This vigilance is not pedantry: nearly every subtle bug in a language definition is a place where the two languages were quietly conflated.

Meaning as a map from syntax to mathematics

The cleanest picture of a semantics is a function from syntax to mathematics. On the left sit the well-formed expressions of the object language; on the right sit mathematical values. The semantics is the arrow between them — traditionally written with the Scott brackets \llbracket \cdot \rrbracket, so that \llbracket e \rrbracket reads "the meaning of e". Different, distinct object expressions may land on the same value — \llbracket 2+3 \rrbracket = \llbracket 7-2 \rrbracket = 5 — exactly because meaning collapses surface differences that do not matter.

This "two-column" mental model survives all three semantic styles below. They differ only in what the right-hand column contains and how the arrow is computed: another program state (operational), a mathematical function (denotational), or a logical assertion about before and after (axiomatic).

A running example: the language of arithmetic expressions

Almost every idea in this course can be rehearsed on a language so small it fits in a line — the arithmetic expressions, often called Exp or AExp. Its abstract syntax:

e \;::=\; n \;\mid\; e_1 + e_2 \;\mid\; e_1 \times e_2

Read the ::= as "is one of" and the \mid as "or". An expression is either a numeral n, or a sum of two smaller expressions, or a product of two smaller expressions. That is a complete grammar — and, read as a recipe for building trees, a complete inductive definition of the set of expressions. We will make that inductive reading precise in the next lessons; for now, notice that every expression is finite and built from strictly smaller pieces, which is exactly what lets us define its meaning by recursion.

Here is the meaning, given compositionally — the value of a compound expression is built from the values of its parts, using the corresponding metalanguage operation:

\llbracket n \rrbracket = n \qquad \llbracket e_1 + e_2 \rrbracket = \llbracket e_1 \rrbracket + \llbracket e_2 \rrbracket \qquad \llbracket e_1 \times e_2 \rrbracket = \llbracket e_1 \rrbracket \times \llbracket e_2 \rrbracket

Look hard at the middle equation. The + on the left is object syntax — a symbol in the program. The + on the right is honest integer addition in the metalanguage. The whole equation says "to find the meaning of a syntactic sum, take the meanings of the parts and really add them." That is the object/metalanguage border, in a single line.

Running the definition by hand

Let us compute \llbracket (1+2)\times 2 \rrbracket the way the equations demand — outside in, replacing each expression by the meaning of its parts until only metalanguage arithmetic remains:

\llbracket (1+2)\times 2 \rrbracket = \llbracket 1+2 \rrbracket \times \llbracket 2 \rrbracket = \big(\llbracket 1 \rrbracket + \llbracket 2 \rrbracket\big) \times 2 = (1 + 2) \times 2 = 6.

And here is the very same definition transcribed into TypeScript. The Exp datatype is the abstract syntax; the meaning function is \llbracket \cdot \rrbracket; and the ordinary + and * in the recursive cases are the metalanguage operations. Press Run:

// Abstract syntax of the tiny expression language (the OBJECT language). type Exp = | { kind: "num"; value: number } | { kind: "add"; left: Exp; right: Exp } | { kind: "mul"; left: Exp; right: Exp }; // Convenience builders. const num = (n: number): Exp => ({ kind: "num", value: n }); const add = (l: Exp, r: Exp): Exp => ({ kind: "add", left: l, right: r }); const mul = (l: Exp, r: Exp): Exp => ({ kind: "mul", left: l, right: r }); // The semantic function ⟦·⟧ : Exp → number (the METALANGUAGE side). function meaning(e: Exp): number { switch (e.kind) { case "num": return e.value; // ⟦n⟧ = n case "add": return meaning(e.left) + meaning(e.right); // real + on the right case "mul": return meaning(e.left) * meaning(e.right); // real * on the right } } // (1 + 2) * 2 const program: Exp = mul(add(num(1), num(2)), num(2)); console.log("⟦(1+2)*2⟧ =", meaning(program)); // 6 // Two DIFFERENT expressions, ONE meaning: 2+3 and 7-... well, 1+4. console.log("⟦2+3⟧ =", meaning(add(num(2), num(3)))); // 5 console.log("⟦1+4⟧ =", meaning(add(num(1), num(4)))); // 5 — same value, different syntax

Notice the recursion follows the grammar exactly: one case per production. That is no accident — it is compositionality, and it is the deep reason a semantics can be both finite (a handful of equations) and total (defined on infinitely many programs). We will return to this shape again and again.

Three styles of meaning

There is more than one useful mathematical object to call "the meaning". The three classical schools — which the rest of the course develops in depth — answer the question "what does a program mean?" differently, and each is best at a different job.

Style	Meaning is…	Answers the question	Best for
Operational	a sequence of computation steps on an abstract machine (a transition relation)	"how does it run?"	implementing interpreters; type-safety proofs
Denotational	a mathematical value/function the program denotes, built compositionally	"what is it, abstractly?"	reasoning about equivalence; program logic foundations
Axiomatic	logical assertions relating the state before and after (pre/postconditions)	"what is true afterwards?"	verification; proving programs correct

Crucially, these are not rival theories of the same language so much as complementary tools: for a well-designed language they agree, and a large part of semantics is proving adequacy and full abstraction theorems that say so — that the operational and denotational meanings match. Our little \llbracket \cdot \rrbracket above was denotational (it mapped straight to numbers); in the next lessons we will give the same language an operational semantics with inference rules, and check the two coincide.

Constantly — the history of language design is a graveyard of underspecified corners. C's notorious "sequence points" left expressions like i = i++ + 1 with undefined behaviour: the standard genuinely did not say what they mean, so different compilers produced different results and the committee simply declared such programs erroneous. ALGOL 60, by contrast, was defined with unusual care yet still harboured a famous ambiguity in its call-by-name parameter rule (the "Jensen's device" surprises). The lesson the field drew is stark: prose specifications, however careful, leak. When Milner's team built Standard ML in the 1980s they did something almost unheard of — wrote The Definition of Standard ML, a complete formal operational semantics as inference rules, the whole language, no prose hand-waving. It remains the gold standard for what "define a language" should mean, and modern efforts (WebAssembly ships with a formal semantics; CompCert is a proven-correct C compiler) follow directly in its footsteps.

The commonest confusion at this stage is to blur syntax and meaning — to think that the expression 2+3 "is" the number 5. It is not. 2+3 is a tree of symbols; 5 is a number in the metalanguage; the semantics \llbracket \cdot \rrbracket is the bridge between them, and it is a genuine, non-trivial object. The tell-tale symptom is a sentence like "obviously 2+3 equals 5" — obvious to you, because you already carry the arithmetic semantics in your head, but a computer knows only the tree until the semantics tells it otherwise.

A second, subtler slip: assuming every program has a meaning. Introduce division and \llbracket 1 / 0 \rrbracket is undefined; introduce loops and some programs never terminate, so their meaning is not an ordinary value at all. A serious semantics must say what happens in those cases — which is precisely why denotational semantics reaches for Scott's domains with a special "undefined" element \bot, and why operational semantics is comfortable with a relation that simply gets stuck or runs forever. "It always gives a number" is an assumption to earn, not to assume.