An experimental optimizing compiler written by LLM
Note: This project is currently in an experimental stage. External pull requests are not accepted at this time.
Tuffy explores several unconventional compiler design ideas:
- Infinite precision integers (idea by inclyc) — The IR uses a single
inttype with no fixed bitwidth. Arithmetic operates on mathematical integers; signedness and minimum required bits are derived at use sites. This eliminates zext/sext/trunc noise and lets optimization passes focus on mathematical equivalence. - Analysis is also a transformation (idea by inclyc) — Static analyses are not separate passes that feed information to optimizations. Instead, analyses are expressed as transformations on the IR itself, unifying the two and reducing phase ordering problems.
- Declarative, verified optimizations — Transforms are declarative rewrite rules, not hand-written IR manipulation. Every rule has a machine-checked correctness proof in Lean 4 against the formal IR semantics. A codegen generator produces Rust implementation from verified rules, minimizing the trusted code base.
- Formal-first — Correctness of optimization passes is backed by formal verification from the start, not bolted on after the fact. The IR semantics are designed to be amenable to automated reasoning.
- Hardware-friendly IR — Explore IR representations that are more cache-friendly and suitable for modern hardware, reducing pointer chasing and improving data locality during compilation.
- Policy-mechanism separation — Optimization strategies are decoupled from the compiler engine. Users can specify or pin a particular optimization policy (e.g., lock to a versioned strategy) to prevent performance regressions when upgrading the compiler.
- 2026-02-08 — Project started
- 2026-02-09 — Successfully compiled and ran "Hello, world!" via
rustc -Z codegen-backend