Current limitations

Albite is a research language at 2.0-beta. This page is the honest inventory — what is missing, and what is currently wrong. It is more useful than a feature list, because a confidently wrong claim costs a reader far more than a missing one.

Everything below was checked against the compiler while this page was written, not copied from a changelog — against v1.5, again against 2.0-alpha, and again against v2.0.0-beta.3.

Two compilers ship, and they do not yet agree. On Linux, albite is the Rust bootstrap. On macOS, albite is the self-hosted compiler and the bootstrap sits beside it as albite-bootstrap. Where this page says “the self-hosted compiler”, it means the macOS albite; when it disagrees with the bootstrap, the bootstrap is right.

Known divergences

These are cases where a compiler produces a wrong answer or refuses a valid program.

The self-hosted interpreter ignores return in statement position

fn f() -> Nat {
    return 5;
    99
}

The self-hosted albite run gives 99. The bootstrap’s run and every compiled binary give 5, which is correct. The compiler even warns that line 3 is unreachable.

return in tail position — if c { return a } else { return b } — is fine.

The self-hosted interpreter cannot run same-named imports

With two sibling modules both exporting label, the self-hosted albite run refuses the program, saying it “cannot yet tell same-named definitions apart”. The bootstrap’s run and compiled output are correct, with a full path (alpha::label()) or an import (use alpha::label).

The self-hosted interpreter prints a try block instead of running it

A try block containing ? — the one shown on Errors — runs under the bootstrap and compiles on both compilers. The self-hosted albite run prints the program’s internal form instead of its value.

Work around all three on macOS with albite-bootstrap run, or by compiling.

The self-hosted compiler does not parse tactic proofs

theorem … by { … } is refused by the macOS albite with expected '{', found 'by'. Check tactic proofs with albite-bootstrap.

Not supported yet

Syntax

• Turbofish in the self-hosted compiler. identity::<Nat>(42) works with the bootstrap, and does not parse in the macOS albite. Annotating the binding or the return type works in both.
• String interpolation. "Hello, {name}" is a literal string containing braces. Use ++ with conversion functions.
• Tuple index access. There is no p.0; destructure with let (a, b) = p;.
• Or-patterns on constructors. Red() | Green() => ... is refused. On numbers they work — 1 | 2 => ... — since 2.0-alpha.
• A record spread needs a type from its context. let r = { ...p, x: 5 }; is refused with cannot infer type; annotate it: let r: Point = { ...p, x: 5 };. The self-hosted compiler refuses a record spread even when annotated (record update not yet fully implemented); use albite-bootstrap.

Type system

• No indexed families — no length-indexed vectors or similar. Planned for v2.1. (Not to be confused with a recursive type nested inside a generic one, which is supported, with one restriction — see A recursive type nested inside a generic one.)
• No refinement types — no { n: Nat | n > 0 }. Planned for v2.1.
• No universe hierarchy. Stratified Type 0 : Type 1 : … is a v2.0 item; until it lands the theory is not known to be consistent the way a mature proof assistant’s is.
• No type classes or traits. Planned for v2.1.
• refl unfolds only what provably terminates. Since 2.0-beta, Eq<Nat, double(2), 4> is provable by refl, within a work limit; a #[partial] function is never unfolded. See Types as propositions.

Proofs

• The tactic language is small. induction, cases, rewrite, bounded simp, ring and omega exist since 2.0-beta; there are no user-defined tactics, and the self-hosted compiler does not parse them yet (above).
• Termination checking is structural only. Since 2.0-alpha every recursive function is checked, by default: some parameter must get strictly smaller, by being taken apart with match, at every recursive call. That is Phase 1 of the checker — there is no well-founded recursion on a measure (halving a number, a cursor moving through a string), and that is why #[partial] exists. See Recursion the compiler can see ends.

Tooling

• No LSP. A minimal implementation is a v2.0 item.
• No package registry. Since 2.0-beta an albite.toml lists local library folders; there is nothing to download packages from.
• No debug info. DWARF output for source-level debugging is a v2.0 item.

Rules the compiler enforces

Not limitations, but the four places a program that looks fine is refused outright. Each has a page with a rejected program, the diagnostic, and what to write instead:

Resolved

If you are reading older material, these were limitations once and are no longer. Two of them were still listed as such in the previous reference documents:

Stability

Semantic versioning covers tooling releases, not the language surface. Breaking changes are expected before v2.0 — this is a beta. See the roadmap.