MiniForth – A small Lean tutorial for programming language semantics

MiniForth teaches language semantics through a tiny Forth in Lean

MiniForth is a Lean tutorial for programming language semantics. The command lake build checks examples and proofs. lake exe miniforth runs the executable. The tutorial starts with MiniForth/Examples.lean; reading the definitions those files use is enough to meet Forth without learning all of Lean first.

Writing Forth programs as Lean terms

Declarations introduce new Forth programs; the instructions after the declarations form the main body. In Lean this is an ordinary term of type Program using the [forthProgram| |] syntax:

def arithmetic : Program := [forthProgram|
  : SQUARE DUP * ;
  : CUBE DUP SQUARE * ;
  : SUM-OF-SQUARES SQUARE SWAP SQUARE + ;
  3 4 SUM-OF-SQUARES
]

The result is [25]. The head of a Lean list is the top of the stack. A Forth program acts on an existing stack: SQUARE sends x :: rest to x * x :: rest, preserving the unused part.

The language has integer literals, +, -, *, =, DUP, SWAP, DROP, calls to named Forth programs, and IF ... ELSE ... THEN. Quotation boundaries are explicit: [forth| DUP *] is a body; [forthDecl| : SQUARE DUP * ;] is one declaration. Hyphenated names and negative literals are supported. Names use Lean identifier segments; an escaped identifier such as «SQUARE-2» is used when a name contains a numeric segment or a reserved keyword. MiniForth names are case-sensitive.

Inside a quotation, a name bound to a Lean local variable pushes its value as an integer; other names call Forth programs. Use {term} to push a Lean expression, such as {a + b}, and CALL name to force a call when names overlap. Primitives retain their meaning and declaration names always name Forth programs. Global Lean definitions require explicit interpolation. These features construct syntax trees parameterized by Lean values; they do not add runtime variables to MiniForth.

How goals and messages display programs

Importing MiniForth.Syntax also makes goals and messages display these quotations. For example, an equivalence goal reads:

⊢ Equiv env [forth| a b +] [forth| b a +]

The printer handles bodies, declarations, whole programs, and nested conditionals. Long quotations wrap and indent to fit Lean's pp.width. Symbolic values keep their Lean bindings; calls use CALL or escaped names when needed. A known prefix with an unknown continuation prints as List.append [forth| SQUARE] rest. Using explicit list append preserves its meaning even with a custom ++ instance. Symbolic instructions or names that the quotation grammar cannot express retain ordinary Lean syntax. Named definitions remain named.

Use set_option pp.miniForth false to inspect the underlying syntax trees during the tutorial. The general options pp.notation false and pp.explicit true also disable Forth notation. The implementation separates parsing and elaboration in Quotation.lean from goal display in PrettyPrinter.lean. The printer tests check that printed text parses and elaborates back to the same expression, including at narrow widths.

Deliberate semantic choices

• Integers are mathematical integers, not bounded machine words.
• In 3 4 - , the result is -1. The top operand is the right operand.
• Zero is false; every nonzero integer is true. = produces -1 or 0.
• IF consumes its condition. Insufficient operands causes stackUnderflow.
• A program has one global dictionary. Forward references and recursion are allowed.
• Linking rejects duplicate declarations and unresolved calls, including calls in unselected branches. Linking checks names, not stack safety or termination.
• LinkCorrectness.lean proves that successful linking prevents runtime errors caused by calls to undeclared Forth programs on every input stack.
• Direct evaluation of an unlinked body can report unknownWord. The semantics remains defined on malformed programs, which lets us state what validation buys us.
• Exhausted fuel means "execution has not finished within this budget." It is neither a runtime error nor a proof of divergence.
• This is a teaching language inspired by Forth, not an implementation of a Forth standard. Its global dictionary does not model an interactive dictionary with successive redefinitions.

Shallow embedding: programs as Lean functions

Read MiniForth/Shallow.lean. A Forth program is a Lean function; composition propagates errors. Proves square_run and use ordinary function equality to express equivalence. Explore the family of Forth programs built with iterate.

A shallow iterate n prog demonstrates host-language abstraction. The host can supply features beyond the MiniForth grammar, so decide which features a model intends to expose before treating every shallow term as a MiniForth program.

Deep embedding: programs as data

Read Basic.lean, Quotation.lean, and Link.lean. The same Forth program is now data. Inspect the AST and separate parsing, name checking, and execution. Quotation is convenient notation, not a new semantics.

Big-step and small-step semantics

Read Deep.lean. Big-step derivations describe completed computations; small steps expose each transition. Follow a call and a branch, then a recursive Forth program. Connect the relations to the executable evaluator and explain why a fuel limit does not define the language's meaning.

Recursion.lean proves factorial correct for every natural input. Divergence.lean proves that FOREVER never produces any result.

Program equivalence

Start with ProgramEquivalence.lean: prove familiar algebraic laws between quoted programs. Then read Equivalence.lean, prove a local optimization, and lift it through sequencing. Compare SWAP SWAP with the empty body, including short input stacks. Discuss why a correct optimizer must preserve failures.

Connecting the embeddings

Read Denote.lean. Translate deeply embedded Forth programs into shallow functions using denote. Supply the meanings of calls through prog, prove correspondence under CallsAgree, and transfer shallow function equalities to deep program equivalences.

Weakest preconditions

Read WeakestPrecondition.lean and the worked contracts in Examples.lean. Calculate backwards through a sequence. Separate successful termination (total correctness), partial correctness, and safety. Then read Conditionals.lean: its exact precondition shows how the required stack depth can depend on which branch is selected.

Automation with grind

Compare the original proofs with the corresponding files in MiniForth/Grind/. Study which semantic rules are registered, then let grind handle routine reasoning. Keep induction, useful contracts, and recursive-call unfolding visible as choices made by the engineer.

The order intentionally introduces declarations before recursion. The initial arithmetic examples need no recursive definitions; branching and recursion are available when the class is ready for them. The longer infrastructure proofs in Deep.lean and LinkCorrectness.lean can be an optional second pass. The first lessons only need to read their statements and work with the smaller program proofs in Shallow.lean and Examples.lean.

| Feature                    | Original lesson          | Automated version       |
|----------------------------|--------------------------|-------------------------|
| Shallow functions and algebra | Shallow.lean             | Grind/Shallow.lean      |
| Program equivalence        | ProgramEquivalence.lean  | Grind/ProgramEquivalence.lean |
| Arithmetic contracts and constant folding | Examples.lean | Grind/Examples.lean |
| Weakest preconditions      | WeakestPrecondition.lean | Grind/WeakestPrecondition.lean |
| Hoare triples and verification conditions | VerificationConditions.lean | Grind/VerificationConditions.lean |
| Conditional stack requirements | Conditionals.lean | Grind/Conditionals.lean |
| Terminating recursion      | Recursion.lean           | Grind/Recursion.lean    |
| Divergence                 | Divergence.lean          | Grind/Divergence.lean   

The shared annotations expose generic semantic facts. Each lesson then proves its own contracts and can register them locally for subsequent proofs. For example, square_step describes a call to SQUARE with an arbitrary continuation; cube_step uses that contract. The equivalence of a CUBE and a SQUARE a * then follows with by grind, without expanding either dictionary entry again.

grind combines these facts with equality reasoning, case analysis, and integer arithmetic. The program-equivalence file derives commutativity, associativity, distributivity, and stack rewrites directly. The conditional lesson also proves:

example : Equiv env [forth| DUP IF 1 + ELSE DROP 1 THEN] [forth| 1 +] := by
  grind

Here the zero-branch condition explains why replacing the top value with 1 agrees with incrementing it. The proof also covers empty-stack underflow.

For a Hoare triple, forth_wp applies the WP rules and leaves the resulting verification condition. Import MiniForth.Grind.Tactics to use it:

example (env : Env) (n : Int) :
    Hoare env (fun s => s = [n + 1]) [forth| DUP *]
      (fun s => s = [n * n + 2 * n + 1]) := by
  forth_wp
  -- ⊢ (n + 1) * (n + 1) = n * n + 2 * n + 1
  grind

The tactic also handles standalone WP goals, symbolic stack shapes, and conditionals. It uses proved equations and simp, which may close trivial conditions immediately. forth_wp [body, contract] can unfold a named program body or use an exact WP contract. A Hoare theorem alone gives a sufficient precondition, rather than an exact WP equation. Calls without supplied contracts remain WP obligations; rw [wp_call lookup] expands one call explicitly.

Recursive Forth programs still require induction and a termination argument.

What the executable prints

The executable prints both arithmetic results, conditional addition, factorial, validation errors, underflow, an exhausted run, and a small-step trace of 3 SQUARE.

Translating deep programs to shallow functions

Denote.lean connects the two representations. denote prog code translates a deeply embedded Forth program into a Shallow.Prog. It maps primitives to their independent shallow implementations, sequences to composition, and conditionals to Shallow.branch. The supplied prog : String → Shallow.Prog gives the meanings of named Forth programs.

denote_append proves that concatenation becomes composition. Under CallsAgree env prog, denote_correct relates the resulting function to big-step evaluation, including errors, and equiv_iff_denote_eq relates deep equivalence to function equality. The examples translate SQUARE, CUBE, and a conditional, then reuse Shallow.double_eq to prove DUP + equivalent to 2 *.

The call agreement assumption requires every call to return a result on every stack; it cannot hold for a deep environment with a divergent call.

Conditional stack requirements

Conditionals.lean pairs these definitions:

def addWhen : Shallow.Prog := Shallow.branch Shallow.add Shallow.skip
def program : Program := [forthProgram|
  : ADD-WHEN IF + ELSE THEN ;
  10 20 -1 ADD-WHEN
]

Both produce [30]. ADD-WHEN consumes its flag. With zero it leaves the rest of the stack alone; with any nonzero integer it adds the next two values. Consequently [0] succeeds with [], while [-1] causes underflow.

The correspondence theorem covers every stack and every outcome. The exact WP requires a flag, then either a zero flag with the postcondition already true of the remaining stack, or a nonzero flag with two operands whose sum establishes the postcondition. Requiring three entries on every input would exclude valid calls with a zero flag.

The shallow version reuses ordinary functions; the deep version exposes a branch as syntax. The example also proves that IF + ELSE THEN is equivalent to 0 = IF ELSE + THEN: negating the condition and exchanging the branches preserves successes and errors, including for nonzero flags other than -1.

Equivalence proofs in program notation

ProgramEquivalence.lean contains proofs in the notation used to write the programs themselves:

open MiniForth MiniForth.Deep
example (env : Env) (a b : Int) :
    Equiv env [forth| a b +] [forth| b a +] := by
  intro s r
  simp [Prim.eval, Int.add_comm]

Here a and b are arbitrary Lean integers inserted as literal-push instructions. Introducing s and r asks Lean to compare the two programs on every initial stack and every outcome. Simplifying execution reduces the proof to an integer law.

The file also proves multiplication commutativity, addition associativity, distributivity, duplication and push/drop rewrites, and combining two offsets: a + b + is equivalent to {a + b} +, including on the empty input stack.

Another theorem reuses addition commutativity inside arbitrary surrounding code.

The counterexample 0 + versus an empty body shows where an arithmetic identity alone is insufficient: the addition can underflow.