v2.0.0-beta.3

v2.0.0-beta.3

Covers v2.0.0-beta.1 … v2.0.0-beta.3, the first releases as Albite; the 2.0.0 alphas were published as Tungsten.

v2.0.0-beta.3 — 2026-10-28

Fixed

• Every cargo command works on a fresh clone again: the workspace listed the crate behind the deprecated tungsten command as a default member without publishing it, so cargo refused the whole workspace. That crate is now published with the rest of the source

v2.0.0-beta.2 — 2026-10-28

Fixed

• The Linux release archive builds again: tungsten-docker.sh, the old name that forwards to albite-docker.sh, is published with the rest of the source

v2.0.0-beta.1 — 2026-10-28

Tungsten by Spinning Cat Studios is now Albite. The tungsten command, TUNGSTEN_* settings and tungsten.toml keep working throughout 2.0.x and are removed in 2.1.

The manual, and a playground where its examples can be edited, checked and run on the beta in the browser, now live at albite-lang.com.

Added

Language

• Tactic proofs: theorem … by { … } proves a statement step by step, and every proof built that way is re-checked by the proof kernel
• Tactics rewrite (by an equation, in either direction), induction, cases, bounded simp [lemmas], ring (normalises a Nat equation, including known powers) and omega (bounded linear Nat goals); a tactic that does not apply or leaves goals open is an error (E0082, E0083, E0085–E0088)
• Tactic proofs can state existential and family goals, give a witness, and prove the rest step by step
• Dependent function types: a signature can name its parameters in its result, written (x: A) -> B, and each use fills in its argument; a constructor payload or record field may not declare one (E0025)
• Existential statements: a dependent pair and exists, whose proof is a witness paired with evidence, and which a proof can take apart again (E0065 when the binder is not data)
• Propositions are their own sort: Le and Lt are declared as families taking arithmetic expressions, and a definition can quantify over a predicate (E0066–E0069, E0023 for a term used as a type)
• Disjunction in proofs: build an "or" from either side and split one into its cases (E0024)
• The proof kernel treats true = false as impossible, so a mismatch between distinct constructors can be refuted
• Arithmetic library: named and cited addition, multiplication and order lemmas; Divides and its lemmas; binomial coefficients with Pascal's rule; division and remainder (nat_div, nat_mod, mod_def); powers and finite sums; primes and Euclid's lemma; a prime divides its binomial coefficients; strong induction; and the binomial theorem
• let mut bindings can be reassigned, including inside branches; reassigning an immutable binding (E0104), capturing a mutable one in a closure (E0105) or reassigning one inside a region (E0106) is refused
• region { e } frees everything allocated inside the block when it ends, by any exit; a result that could outlive its memory, or a region inside a proof, is refused (E0094–E0096), and a region may return any first-order value, which is copied out before the memory goes
• A resource handle is used once: using it after it was consumed (E0092) or capturing it in a closure (E0093) is refused, on both compilers
• Packages: an albite.toml manifest lists local library folders, each used by name; a library can have its own dependencies, a shared one is loaded once, and an invalid manifest, a missing dependency, a name clash or a dependency cycle is refused (E0120–E0124)
• A file's sibling modules are found without an explicit path
• (macOS) The shipped self-hosted compiler reads its sibling modules, a package manifest and its libraries, and enforces the same package boundaries
• (macOS) The shipped self-hosted compiler accepts dependent signatures, a dependent induction motive and the whole arithmetic library

Runtime

• Joining strings, appending to an owned string, reading the program's arguments and the integer-overflow trap are written in Albite itself and on by default, at the speed of the previous versions
• Each empty constructor of a recursive type is one shared read-only cell instead of a fresh allocation
• Sums of at most eight bytes pass and return in registers
• A compiled program carries only the runtime code it calls
• A compiled program runs on a 512 MiB stack it sets up itself, so how deep it can recurse no longer depends on the shell that starts it; ALBITE_STACK_SIZE (e.g. 8M, 2G) changes the size, and an invalid value stops the program with a message before it runs

Tooling

• --error-format=json writes machine-readable diagnostics, one versioned record per line, with location, notes, help and a suggested next command, for check, run and compile
• albite test --format json|junit writes one record per test plus a summary, or a JUnit XML report for CI dashboards
• albite test exits 0 when every test passed, 1 when a test failed, and 2 when the run could not produce verdicts
• A build failure has a kind and a code (E0140–E0146) that albite explain error knows
• Every syntax error carries its own code (E0110–E0117)
• A test file beside its module (foo_test.tg next to foo.tg) joins that module when tests run, and every other command ignores it
• check counts the theorems resting on an axiom or a sorry and names what each one rests on
• albite doctor check proof kernel-census <file> runs every proof-relevant definition through the proof kernel and sorts each refusal by cause; albite diff kernel-census compares two saved runs
• albite doctor check proof term-size <file> lists definitions beside the size of their proof or Core term, ranked; albite diff term-size compares two saved runs
• albite doctor check sorry-sites accepts a directory and prints one line per program with a total
• albite doctor check module name-collisions reads every package the compiler would load
• (macOS) The shipped self-hosted compiler writes JSON diagnostics and JSON and JUnit test reports, and its errors and syntax errors carry their catalogued codes
• (macOS) The shipped self-hosted compiler's check reports sorry holes and axioms

Changed

• The compiler command is albite, and the self-hosted stages are albite1 and albite2; the release archives ship albite, albite-bootstrap (macOS) and albite-docker.sh. The tungsten command and tungsten-docker.sh still work and print one notice per run (none under --error-format json)
• A project's manifest is albite.toml; a tungsten.toml is still read, with a note to rename it (or that it is ignored, beside an albite.toml). The build cache is .albite/, a .tungsten/config.toml is read until .albite/config.toml exists, and cache clean removes both directories. The sidecar feedback store moves once from ~/.tungsten/sidecar to ~/.albite/sidecar
• Every setting is read as ALBITE_* first (ALBITE_ARENA, ALBITE_STACK_SIZE, ALBITE_TERMINATION, ALBITE_NO_CACHE, …); the old TUNGSTEN_* name still works when the new one is unset or empty, and prints one notice per name per run. An empty value now counts as unset
• The compiler's crates are albite_core, albite_codegen, albite_runtime and albite_bootstrap (cargo build -p albite_bootstrap), and the runtime archive a compiled program links is libalbite_core.a. The runtime's own symbols are __albite_* and a program's entry symbol is albite_main; a program may define neither, nor the names they replace, throughout 2.0.x
• Every theorem and lemma is re-checked by the proof kernel, and a refusal is an error (E0081), as is an exemption entry the build contradicts (E0084); the kernel simplifies both sides before giving up, substitutes under a dependent motive, splits on a constructor, reads records by their encoding, and refuses what the elaborator refuses
• Proofs may unfold functions proven to terminate, on concrete arguments and under a variable, within a work limit; functions not shown to terminate stay sealed
• Induction checks each case against its own goal, so 0 + n = n is provable
• A closed numeral sum inside a family argument reduces, so "at most 2 + 3" and "at most 5" are the same statement
• A function whose result holds a fact is checked like a theorem, so a false one is refused where it is written
• A proof may not rely on a call to code outside the language
• Two definitions of one name in a file are refused, naming the first
• Two modules may offer the same value name; a full path always runs the function it names, and a bare name that could mean either is refused (E0019)
• let mut is accepted, so the former "mutability not supported" error is gone
• A match on a type parameter with a single case is refused, as the many-case form already was
• A guard on an arm of a match over a data type is refused instead of being silently dropped
• A constructor of another type in a pattern is refused, naming both types
• A type parameter applied to arguments is refused (E0068)
• Positions in text count bytes everywhere: substring gives one answer on every reader, a cut inside a multi-byte character traps, and char_at past the end is zero
• A compiled Nat division or remainder by zero gives zero, as the interpreter and the proof kernel do
• (macOS) The shipped self-hosted compiler refuses a non-exhaustive match, an incomplete or multi-field nested pattern, a pattern naming an unknown constructor, two values sharing a name, private and duplicate imports, an ambiguous bare value, a proof relying on foreign code, and a second use of a resource handle joined from branches, as the Linux build does
• (macOS) The shipped self-hosted compiler stops adding errors after the first in each broken definition, and no longer cascades on two common mistakes

Fixed

• A return that is not in tail position leaves the function in the interpreter, as in compiled programs
• A ? inside a try block stops at the block instead of returning from the function
• A bare nullary constructor inside a pattern means the same as its spelling with empty brackets
• A nested arm with no catch-all for its missing cases is refused as incomplete instead of running a hole
• A match's catch-all name holds the whole matched value
• The interpreter keeps the operator it steps and stops at overflow, so a false equation is refused
• A function named like a C library symbol no longer captures the runtime's own calls
• A positivity violation is reported once, in the file that defines the type
• A termination error in a proof names the proof's own file and line, once
• A library reached by two import paths is checked once
• Three programs only one compiler refused get one verdict on both, including a miscompile
• albite info def --callers counts uses in theorem statements
• The self-hosted compiler checks and builds its own source within the usual 8 MB stack, instead of overflowing it on Linux
• (macOS) Each case of a match with a gapped catch-all runs its own code
• (macOS) The catch-all of a nested group covers the inner cases the arms leave out
• (macOS) A program that builds a value with a multi-argument constructor and reads it back runs
• (macOS) Termination checking sees a recursive data type however it is encoded