Side-by-side comparisons of Go syntax with two Lean encodings:
* Surface AST (GolangLean.Expr) — mirrors go/ast.Node from upstream.
* Tiny Go Core (GolangLean.Core.Term) — kernel calculus with proven
operational + type semantics.
Twelve sections covering: literals, arithmetic, comparison, conditional,
variables/let-binding, functions/application, references/deref/assign,
sequencing. Each example includes a `#eval` running the term through
the proven Core.eval; output matches what's expected at run time.
Demonstrated programs:
- `(5 + 3) * 2` → 16
- `let x = 3 in let y = 7 in x < y` → true
- `(λ x. x*2) 21` → 42
- `let double = λ x. x*2 in double (double 5)` → 20
- `let p = &42 in *p = 100; *p` → 100 (heap: [vInt 100])
- higher-order: `(λ f. λ x. f (f x)) double 3` → 12
Each #eval is a runtime witness for a Core.BigStep derivation. Apply
Core.eval_sound to get a proof of the BigStep relation, and
Core.preservation to get the value's type.
Supporting changes:
- Added Repr instances for Core.Value and Core.EnvList (manual,
handling the mutual inductive — derive doesn't compose across the
mutual block).
- Added RosettaStone as a lean_lib in lakefile.toml.
GolangLean/Core/Preservation.lean:
theorem preservation:
HasType Γ e T -> HasTypeH ht h -> HasTypeEnv ht env Γ ->
BigStep h env e v h' ->
∃ ht', HeapTy.extends ht ht' /\ HasTypeH ht' h' /\
HasTypeV ht' v T /\ HasTypeEnv ht' env Γ
The standard big-step type-soundness result: well-typed terminating
programs produce well-typed values, with heap conformance preserved.
Proof is by induction on the big-step derivation, fourteen cases.
Supporting infrastructure:
HeapTy.extends_push - heap-typing extends across a push
HasTypeH.push - heap conformance preserved by push
HasTypeH.setIfInBounds - heap conformance preserved by in-bounds update
binop_apply_sound - operator typing matches operator semantics
The closure case (appR) uses the mutual HasTypeV/HasTypeEnv weakening
lemmas from TypeSoundness to thread heap-typings across the three
sub-derivations. The assign case (assignR) uses the heap-update
lemma to preserve conformance. The if-cases collapse the cross-rule
(ifT vs ifF) ambiguity via Bool.noConfusion on the condition's IH.
Zero sorries / axioms / admits across the project. Full lake build clean.
Phase A — GolangLean/Core/Eval.lean:
def eval : Nat -> Heap -> Env -> Term -> Option (Value x Heap)
Fuel-bounded recursive evaluator, total over the fuel.
theorem eval_sound: eval succeeds => BigStep holds.
Bridges executable computation to inductive specification.
Phase B — GolangLean/Core/Types.lean:
inductive Ty {unit, int, bool, arrow, ref}
TyEnv := List (String x Ty); BinOp.typeOf
inductive HasType : TyEnv -> Term -> Ty -> Prop
Standard simply-typed lambda calculus + ML-style references.
Phase B — GolangLean/Core/TypeSoundness.lean:
abbrev HeapTy := Array Ty
mutual inductive HasTypeV / HasTypeEnv (value & env typing under heap-typing)
def HasTypeH (heap conforms to heap-typing)
def HeapTy.extends (prefix-extension of heap-typings)
thm HeapTy.extends_refl, extends_trans
thm HasTypeV.weaken, HasTypeEnv.weaken (mutual; under heap-typing extension)
thm HasTypeEnv.lookup_correspondence (well-typed env yields well-typed values)
The preservation theorem itself
HasType /\ HasTypeH /\ HasTypeEnv /\ BigStep
==> ∃ ht', extends /\ HasTypeH' /\ HasTypeV' /\ HasTypeEnv'
is the next deliverable; the infrastructure here is what its proof
case-analysis depends on.
Zero sorries / axioms / admits across the project. Full lake build clean.
GolangLean/Core/ holds a small calculus that surface Go is intended to
desugar into. Three files:
Syntax.lean - Term, BinOp; thirteen syntactic forms covering
let-binding, lambda, application, references
(Go's & / *), conditionals, sequencing.
Semantics.lean - Value, EnvList, Heap, BinOp.apply, BigStep relation.
Heap is Array Value; references are indices.
Closures capture EnvList lexically, as in Go.
Fourteen big-step constructors, one per syntactic form
(with ifte split into ifTR / ifFR).
Determinism.lean - theorem BigStep.deterministic:
BigStep h env e v1 h1 -> BigStep h env e v2 h2 ->
v1 = v2 /\ h1 = h2
Proof by induction on the first derivation, case
analysis on the second. The ifTR/ifFR cross-cases
close by contradiction via Bool.noConfusion.
No sorries, no axioms, no admits. The kernel is small enough to extend
compositionally: each new syntactic form adds one constructor and one
case to each proof. Type system and concurrency layer come later.
Strategic note: this kernel is shaped so the same construction will
work for any sequential calculus. When octive-lean grows a parallel
Tiny Octave Core, the determinism proof's structure will line up
case-for-case where the languages share constructors. That alignment
is the seed of the cross-language layer.
Mirrors the layout of octive-lean: lakefile, justfile, gitignored
upstream clone, a top-level library module, and a Main entry point
that switches between REPL and file execution.
Module skeleton in GolangLean/:
Token, AST — real ports of go/token and go/ast
Scanner, Parser — stubs throwing notImpl, point at upstream
Value, Env, Error — runtime data shapes
Eval, Builtins, REPL — stubs that compile and run as a placeholder
PureEval, BigStep,
ValueEquiv — formal-semantics layer (mirroring octive-lean)
where cross-language proof eventually lives.
The proof layer is shaped identically to octive-lean's so that
theorems about Go semantics will share their form with the Octave
ones — that shared shape is the candidate for the future
cross-language core.
Upstream reference go-upstream/ (shallow clone of golang/go) is
gitignored.
