LeanRustLisp (LRL) 0.1 Alpha

LeanRustLisp (LRL) is an experimental language that combines:

• dependent types and proof-aware checking
• ownership and borrow checking
• hygienic Lisp-style macros

LRL is currently in alpha. The compiler pipeline is usable, but the language surface, prelude, and backend coverage are still evolving.

Current State (Codebase-Backed)

Implemented in the current tree:

• Workspace crates: kernel, frontend, mir, codegen, cli
• End-to-end pipeline: parse -> macro expansion -> elaboration -> kernel checks -> MIR lowering -> MIR typing/ownership/NLL checks -> Rust codegen
• CLI modes:
  • interpret a file
  • interactive REPL
  • compile to native binary (typed, dynamic, auto backend modes)
• Macro tooling (--expand-1, --expand-full, --trace-expand, --trace-macros)
• Axiom tracking and opt-in execution for axiom-dependent definitions
• Definitional equality fuel control (--defeq-fuel, LRL_DEFEQ_FUEL)

Alpha constraints you should expect:

• Syntax is not fully frozen yet; follow the syntax contract doc linked below.
• compile and compile-mir default to --backend auto (typed-first, fallback to dynamic with warning when needed).
• compile-mir is a legacy name; it still runs the full compile pipeline and emits a binary.
• Prelude loading uses a shared API + backend platform layers:
  • stdlib/prelude_api.lrl + stdlib/prelude_impl_dynamic.lrl (dynamic / interpreter / REPL)
  • stdlib/prelude_api.lrl + stdlib/prelude_impl_typed.lrl (typed / auto compile)
• You may see startup warnings from prelude axiom/primitive declarations in alpha workflows.

Stdlib Status (Alpha)

• Milestone-1 core surface is present in shared stdlib modules:
  • core: Nat/Bool helpers
  • data: List/Option/Result/Pair basics
  • control: minimal Comp helpers (comp_pure, comp_bind)
• Prelude loading now includes shared core/data stdlib modules plus backend platform layer:
  • typed/auto: prelude_api + std/core(nat,bool) + std/data(list,option,result,pair) + prelude_impl_typed
  • dynamic: prelude_api + std/core(nat,bool) + std/data(list,option,result,pair) + prelude_impl_dynamic
• std/control/comp.lrl exists as an alpha helper module but is not in the default prelude stack yet.
• Current backend caveat:
  • typed backend is the primary target for Option/Result/Pair alpha smoke workflows
  • Option/Result helper behavior is currently guaranteed only for the smoke-tested positive paths
  • dynamic overlap remains conservative (Nat/Bool/List-first)

Quick Start

Prerequisites

• For prebuilt CLI binaries: no repo build step is required.
• For compile / compile-mir: Rust (rustc) is still required.
• For building from source: Rust toolchain (cargo, rustc).

Use prebuilt binary package (no cargo build)

This repository now includes a host-target package under:

• dist/aarch64-apple-darwin/

The package layout is:

• cli (prebuilt executable)
• stdlib/ (runtime prelude + stdlib files)

Run from inside the package directory so relative stdlib/... paths resolve:

cd dist/aarch64-apple-darwin
./cli --help
./cli run /absolute/path/to/program.lrl --backend typed

If you use compile or compile-mir from that binary, rustc must be installed because those commands invoke Rust compilation.

CI native binary packages (Linux/Windows/macOS)

GitHub Actions now builds native release binaries with a matrix on:

• ubuntu-latest
• windows-latest
• macos-latest

Workflow file:

• .github/workflows/native-binaries.yml

How to trigger:

• Manual run: GitHub -> Actions -> Native Binary Packages -> Run workflow
• Release-tag run:

git tag v0.1.0
git push origin v0.1.0

Where binaries are published:

• Manual runs: workflow artifacts named leanrustlisp-<target-triple>
• Tag runs: GitHub Release assets (*.tar.gz bundles per target)

Windows package note: executable name is cli.exe; Linux/macOS use cli.

Build

cargo build

Run a program (run command)

cargo run -p cli -- run tests/simple_test.lrl

For visible print side effects, use typed backend:

cargo run -p cli -- run tests/hello.lrl --backend typed

Notes:

• run defaults to --backend dynamic.
• --backend typed for run is currently supported for direct .lrl file targets.
• Program entry is a top-level definition (the last deployed def), for example:

(def main Text
  (print "Hello, world!"))

A bare top-level expression like (print "Hello, world!") is not used as executable entry.

Run a program (interpreter shortcut)

cargo run -p cli -- tests/simple_test.lrl

Start REPL

cargo run -p cli --

Inside REPL, run :help to list commands (:load, :type, :eval, :expand-*, :panic-free, :axioms, ...).

Compile to binary

cargo run -p cli -- compile tests/simple_test.lrl -o build/simple_test_bin
./build/simple_test_bin

Backend selection

# Default (typed-first, dynamic fallback)
cargo run -p cli -- compile tests/simple_test.lrl --backend auto -o build/out_auto

# Force typed backend
cargo run -p cli -- compile tests/simple_test.lrl --backend typed -o build/out_typed

# Force dynamic backend
cargo run -p cli -- compile tests/simple_test.lrl --backend dynamic -o build/out_dynamic

Use --backend auto for normal alpha usage. The dynamic path remains a fallback/debug backend and can still differ from typed behavior outside the documented overlap subset.

Compile via compile-mir command

cargo run -p cli -- compile-mir tests/simple_test.lrl
./output

compile-mir currently compiles and emits ./output by default (unless you use other compile entry points with -o).

CLI Flags You Will Use Often

• --expand-1, --expand-full, --trace-expand: inspect macro expansion for a file
• --trace-macros: print macro expansion trace during normal processing
• --panic-free: reject panic-requiring paths (including interior mutability/runtime borrow checks)
• --macro-boundary-warn: downgrade macro-boundary violations to warnings (user code)
• --require-axiom-tags: require axiom tags (classical/unsafe)
• --allow-axioms: allow running/compiling axiom-dependent definitions
• --allow-redefine: disable prelude freeze guard (unsafe)
• --defeq-fuel N: override definitional equality fuel for this run

Example:

LRL_DEFEQ_FUEL=200000 cargo run -p cli -- tests/simple_test.lrl
cargo run -p cli -- --defeq-fuel 200000 tests/simple_test.lrl

Suggested Alpha Test Commands

cargo test --all
cargo test -p cli --test pipeline_golden
cargo test -p cli --test pipeline_negative
cargo test -p cli --test typed_backend
cargo test -p cli --test backend_conformance -- --test-threads=1

Snapshot-based suites:

INSTA_UPDATE=always cargo test -p frontend
INSTA_UPDATE=always cargo test -p cli

Project Map

• kernel/: core calculus, type checker, definitional equality, kernel invariants
• frontend/: parser, macro expander, desugar/elaborator, diagnostics
• mir/: MIR, typing/ownership/NLL checks, transforms, codegen layers
• codegen/: backend support crate
• cli/: REPL, compile driver, command-line entrypoint
• stdlib/: prelude API/platform files (prelude_api.lrl, prelude_impl_dynamic.lrl, prelude_impl_typed.lrl)
• tests/: .lrl programs for integration/regression
• cli/tests/: pipeline, backend, diagnostics, and conformance tests

Documentation Links

Language and pipeline:

• Syntax contract (draft): docs/spec/syntax_contract_0_1.md
• Kernel boundary / trust model: docs/spec/kernel_boundary.md
• Core calculus: docs/spec/core_calculus.md
• Ownership model: docs/spec/ownership_model.md
• Function kinds (Fn / FnMut / FnOnce): docs/spec/function_kinds.md
• Macro system: docs/spec/macro_system.md
• Phase boundaries: docs/spec/phase_boundaries.md
• Mode boundaries (Total/Partial/Unsafe): docs/spec/mode_boundaries.md

MIR and backend:

• MIR overview: docs/spec/mir/mir.md
• MIR borrows/regions: docs/spec/mir/borrows-regions.md
• MIR NLL constraints: docs/spec/mir/nll-constraints.md
• MIR typing: docs/spec/mir/typing.md
• Typed backend spec: docs/spec/codegen/typed-backend.md
• Prelude API contract: docs/spec/prelude_api.md
• Architecture notes: docs/dev/architecture.md

Diagnostics and examples:

• Diagnostic codes: docs/diagnostic_codes.md
• Example programs: code_examples/
• CLI integration programs: tests/

About

LeanRustLisp (LRL) is an attempt to make three things stop fighting and start cooperating: mathematical truth (Lean), resource reality (Rust), and programmable language (Lisp). The result is a language where you can write high-performance systems code, state the invariants it must satisfy, and then have the compiler refuse to build anything that doesn’t cash those checks.

The basic slogan is: your program is a contract. And LRL’s compiler is a very literal lawyer who insists the contract is internally consistent.

LRL has a small trusted kernel that checks a minimal core calculus (dependent types, universes, inductives). Everything else—parsing, macros, elaboration, borrow checking, optimizations, code generation—is outside the trust boundary. That split matters because it keeps the “truth engine” tiny enough to audit, and it means the fancy parts of the compiler can’t smuggle in unsoundness: they must output core terms the kernel can verify. If you’ve ever watched a compiler become an unreviewable cathedral, you know why this is a civilizational design constraint.

From Lean, LRL takes the idea that types can express theorems. A function’s signature can encode precise invariants: non-empty vectors, dimension-safe matrix multiplication, protocol states, resource budgets. And proofs are not runtime baggage. Proof terms live in Prop and are erased, so you can ship fast binaries that still carry compile-time correctness guarantees. You you can prove sortedness and permutation, then erase the proof and keep the speed.

From Rust, LRL takes the stance that resources are real. Memory, aliasing, mutation, and concurrency are the default failure modes of ambitious software. LRL uses an explicit ownership and borrowing discipline, checked on a dedicated mid-level IR, so safe code can’t create use-after-free, double-free, or data races. The key point is that this safety is part of the language’s semantics, not an accident of one backend. You can transpile to Rust today and target LLVM tomorrow without changing what “safe LRL” means.

From Lisp, LRL takes the refusal to freeze the language. The syntax is designed to be transformed. Macros are first-class: you can define new surface constructs, new notation, tiny DSLs, and new proof automation. But unlike the “wild west” macro cultures of history, LRL aims for hygienic, staged, deterministic macro expansion with good tooling. You get to bend the language without breaking scoping, without breaking error spans, and without turning compilation into a non-reproducible séance.

One of the most important conceptual moves in LRL is the separation of worlds. There is a total fragment—definitions that are allowed to influence types and definitional equality—and a computational fragment—general recursion, IO, allocation, concurrency—that lives under explicit effects. That keeps typechecking decidable and the kernel sane, while still letting you write real programs. The point is to avoid the classic trap: letting “ordinary computation” leak into the logic until the logic becomes a runtime and the runtime becomes a logic and nobody can prove anything without summoning a demon.

Effects are not invisible. In LRL, doing IO shows up in the type. That makes codebases easier to reason about and harder to accidentally corrupt. Also, effects can be capabilities: you hold a token that can be tracked, passed, and restricted. The same machinery can express budgets: fuel, time, memory. At that point, “this computation cannot exceed N steps” stops being a comment and becomes a type-level fact.

What does this buy you in practice? It collapses entire classes of bugs from “things you find in production” into “programs you cannot write.” Out-of-bounds access becomes “type mismatch.” Dangling references become “lifetime violation.” Wrong dimension math becomes “doesn’t compile.” Race conditions become “need a safe concurrency primitive or explicit unsafe.” And the language lets you raise the bar progressively: start with simple static guarantees, then move toward proof-carrying components where it’s worth it.

LRL is also, intentionally, not pretending that safety means “no sharp edges exist.” It means sharp edges are labeled. There is unsafe, and it is explicit. If you cross the boundary into raw pointers or FFI, you’re making a local treaty with chaos, and the compiler will not let you forget where you did that. This is a philosophy as much as a feature: constrain unsafety to small, auditable regions rather than letting it leak everywhere through “temporary hacks” that become permanent.

If Rust is “systems programming without fear,” LRL is “systems programming without fear, plus the option to prove you didn’t lie to yourself.” If Lean is “proofs that compile,” LRL is “proofs that compile into performant programs.” If Lisp is “a language that grows new limbs,” LRL is “a language that grows new limbs and then proves the surgery didn’t break physics.”

License

Dual licensed under Apache-2.0 OR MIT (LICENSE).