FAQ
What is Albite, in one sentence?
A dependently-typed functional language with Rust-flavoured syntax, in which you write a program and prove things about it in the same language, checked by the same pass.
Is it ready to use?
For production work, no. It is a research language at 2.0-beta — a pre-release — breaking changes are expected before v2.0, and it has no package registry, no LSP, and no debugger integration.
For learning, experimenting, or reading a compiler written in its own language, yes — and it is genuinely used, since the compiler is written in Albite and compiles itself.
How is this different from Lean or Rocq?
Those are mature proof assistants with large tactic libraries, extensive mathematical corpora, and years of accumulated work. Albite’s proof surface is far smaller: propositional equality, the equality combinators, induction over naturals, and — since 2.0-beta — a small tactic language and an arithmetic library.
The difference in intent is that Albite is a programming language that can prove things, rather than a proof assistant that can also compute. It compiles to native binaries through LLVM, has a module system and FFI, and is meant to feel like writing Rust. If your goal is formalising mathematics today, use Lean. If it is writing an ordinary program and proving a specific property of it, Albite is aimed at you — though see the limitations first.
How is this different from Rust?
Rust’s type system is not dependent: types cannot mention values, so `Eq<Nat, 2
- 2, 4>` cannot be expressed. Rust gives you memory safety without a garbage collector; Albite does not have a borrow checker yet — that is a v2.1 item.
The syntax is deliberately close. fn, let, match, mod, use and type
mean what you expect, and the novelty is spent on the type system instead.
What does “small trusted core” mean, and why care?
The kernel that checks core terms is about 1,500 lines of Rust. If it is correct, every proof Albite accepts is sound. The parser, elaborator and code generator are much larger, but they sit outside the trusted boundary — a bug in them can make your program fail to compile, but cannot make an unsound proof be accepted.
This is the standard argument for a small kernel, and its value is that soundness has exactly one place to be wrong, small enough for a person to read.
Do I need LLVM?
Only for albite compile. Type checking (albite check) and interpreted
execution (albite run) work without it, which covers most of the writing
loop. See Installing Albite.
Is it self-hosting?
Yes, and verified by a triple-compile fixed point. The Rust bootstrap compiles
the Albite sources to albite1; albite1 compiles the same sources to
albite2; albite2 compiles them to albite3. albite2 and
albite3 are functionally identical.
What is the licence?
MIT.
Who works on it?
Albite is written by Christopher Goddard as an independent research project under Spinning Cat Studios. It is open to sponsorship — see the home page.
Why “AI-friendly diagnostics”?
Error messages carry structured spans, contextual hints, and Levenshtein-based
“did you mean?” suggestions, and albite check --json emits them as
structured data. The reasoning is that an error message is documentation
delivered exactly when it is needed, and that what makes it legible to a
language model — being explicit, structured, and self-contained — is largely
what makes it legible to a person at 2am.
Can I contribute?
The contribution workflow is a v2.1 item, so the project is not yet set up to absorb outside changes well. Bug reports against the current release are welcome via the repository.
Where should I start?
Installing Albite, then Hello, world, then the tour. If you would rather see what makes it different first, read Types as propositions.