crosslang/golang-lean/README.md

golang-lean

A Lean 4 reimplementation of the Go programming language — using the upstream reference compiler/parser as the source of truth, the way octive-lean uses GNU Octave.

Built parallel to octive-lean. Goals:

1. Working Go interpreter for a useful subset (start: pure Go, no goroutines).
2. Formal semantics layered on top: BigStep / PureEval / ValueEquiv so proofs about Go programs are first-class.
3. Cross-language layer — once both this and octive-lean have a real evaluator and big-step semantics, factor a shared core out of two concrete points rather than guessing the abstraction in advance.

Build

lake build

Requires the Lean toolchain pinned in lean-toolchain. elan will pick it up automatically.

Run

# REPL stub
lake exe golang-lean

# Run a .go script (not yet implemented)
lake exe golang-lean path/to/script.go

# Verify the corpus against expected outputs
lake build corpus-check
lake exe corpus-check

Layout

Path	What's there
GolangLean/	Library: Token, Scanner, AST, Parser, Value, Env, Eval, Builtins, REPL, BigStep, PureEval, ValueEquiv, Error
Main.lean	Entry point — REPL or file runner
CorpusCheck.lean	Test driver for corpus/
corpus/	.go test cases paired with .expected outputs
go-upstream/	Shallow clone of golang/go (gitignored, used as reference)

Status

Scaffold. Module skeleton in place. Token and AST are real ports of go/token and go/ast. Scanner / Parser / Eval are stubs that throw notImpl so the project compiles.

Next:

1. Implement Scanner.scan against go-upstream/src/go/scanner/scanner.go.
2. Implement Parser.parseFile recursive-descent against go-upstream/src/go/parser/parser.go.
3. Implement Eval for the pure subset (no goroutines, no defer, no panic/recover).
4. Mirror octive-lean's BigStep / ValueEquiv triple.

Reference

go-upstream/ is a shallow clone of https://github.com/golang/go. Key paths:

Path	What's there
go-upstream/src/go/token/	Token kinds, position tracking
go-upstream/src/go/scanner/	Lexer
go-upstream/src/go/ast/	AST node types
go-upstream/src/go/parser/	Recursive-descent parser
go-upstream/src/go/types/	Type-checker (later)
go-upstream/src/runtime/	Runtime / scheduler / GC (much later)