Roadmap

Albite is an independent research project, so dates are not committed and features ship when they are ready. What follows is direction and sequence rather than schedule.

Shipped

v1.0 (February 2026) — a self-hosted compiler with a verified triple-compile fixed point. See Albite v1.0.
v1.5 (May 2026) — language completeness. Every v1.0 limitation resolved, plus propositional equality and induction. See Albite v1.5.
2.0-alpha (a pre-release) — the first slice of v2.0, for people outside the project: termination checking and the other rules the compiler now enforces, signed integers, a string builder, an arena allocator for compiled programs, and one error per mistake. See Albite 2.0-alpha.
2.0-beta (current, a pre-release) — the first release as Albite: tactic proofs re-checked by a proof kernel, an arithmetic library, let mut, regions, local packages, and machine-readable diagnostics. See Albite 2.0-beta.

v2.0 — production-ready

Making Albite a platform rather than a demonstration: allocation performance, the foundations of proof automation, and the tooling a language needs before anyone else can reasonably use it.

Tactic language foundations — simp, induction, rewrite, cases, and arithmetic decision procedures. The headline proof item, and the thing most likely to change how proofs feel to write. Foundations shipped in 2.0-beta.
Universe hierarchy — stratified Type 0 : Type 1 : …, ruling out Girard’s paradox.
Allocation optimisations — unboxing small ADTs as tagged machine words, region-scoped deallocation on top of the alpha’s arena, string interning. Regions shipped in 2.0-beta.
LSP design and a minimal implementation — go-to-definition, hover, inline diagnostics.
DWARF debug info — source-level debugging in GDB and LLDB.
Package manifest — albite.toml with path dependencies and workspaces. Path dependencies shipped in 2.0-beta.
Diagnostic infrastructure — structured JSON errors, fix-it suggestions, runtime stack traces. JSON errors shipped in 2.0-beta.
Documentation tooling — generated module and function docs.
Native core library — rewriting the albite_core runtime in Albite.
Parallel elaboration — multi-threaded per-module type checking.
let mut (shipped in 2.0-beta) and or-patterns on constructors (on numbers they shipped in the alpha).
Cross-platform release builds and binary-reproducible triple compile.

v2.1 — ecosystem and adoption

Longer-horizon, and dependent on real usage feedback from v2.0.

Type classes / traits — overloading and abstraction
Borrow checker — Rust-style ownership and borrowing
Indexed families — types such as length-indexed vectors
Refinement types — types carrying predicates
Algebraic effects — first-class controlled side effects
Lean4 transpiler — export proofs for independent verification
Full LSP, REPL, and a package registry
Proof irrelevance, row types, and per-definition incremental elaboration
Networking and crypto primitives with type-level protocol modelling
Community contribution workflow

v2.2 — proof language maturity

Closing the gap with mature proof assistants.

Metaprogramming — custom tactics and elaboration extensions written in Albite itself
Notation extensions — user-defined operators and syntax categories
Quotient types — equivalence classes as types
Coercions — automatic conversions via a Coe<A, B> class
Proof library foundations — algebraic hierarchy, order theory, common lemmas

Design principles

These hold across versions and explain most of the choices above:

Small trusted core — new features elaborate to existing core constructs wherever possible, so the kernel stays small enough to audit.
AI-first — rich error messages and structured diagnostics, on the view that both human and machine readers benefit from the same clarity.
Proofs are programs — Curry-Howard throughout, rather than a separate verification layer.
Familiar syntax — Rust and Lean inspired; novelty spent on the type system, not on punctuation.
Incremental adoption — features opt-in where possible.