Albite

Albite 2.0-beta

Albite 2.0-beta, the first release published as Albite. The current build is v2.0.0-beta.3.

A pre-release. The language can still change before v2.0, and GitHub lists this release as a pre-release rather than as Latest. beta.2 and beta.3 fix packaging only; the language is the same as beta.1.

The name changed, the language did not. Earlier releases were published as Tungsten by Spinning Cat Studios. The old command, settings and manifest name keep working, with a notice, throughout 2.0.x, and are removed in 2.1. See About the name for what to rename.

What will surprise you first

  • On macOS, tactic proofs need albite-bootstrap. The macOS archive’s albite is the self-hosted compiler, and it does not parse a by { … } block yet; albite-bootstrap, beside it in the same archive, checks the same file. On Linux, albite is the bootstrap. See Installing Albite.
  • Every theorem and lemma is re-checked by the proof kernel, and a refusal is an error (E0081), never a warning — including a proof the elaborator accepted.
  • Some programs v2.0-alpha accepted are refused: two definitions of one name in a file; a bare name two imported modules both offer (E0019 — a full path still works); a guard on an arm of a match over a data type, which used to be dropped silently; and a match on a type parameter with a single case.

Proofs

  • Tactic proofs. theorem … by { … } proves a statement step by step: induction, cases, rewrite (in either direction), bounded simp [lemmas], ring for Nat equations and omega for bounded linear Nat goals. A tactic that does not apply, or a block that leaves goals open, is an error (E0082, E0083, E0085–E0088). The manual’s proof pages still show proof terms, which is what tactics build.
  • Dependent function types — (x: A) -> B, where the result names the argument — and existential statements, proved by a witness paired with evidence.
  • Propositions are their own sort. Le and Lt are families over arithmetic expressions, and a definition can quantify over a predicate.
  • Disjunction — build an “or” from either side, and split one into cases.
  • Proofs can unfold your functions, when those functions are proven to terminate, within a work limit: refl now proves double(2) = 4, and 0 + n = n is provable by induction.
  • An arithmetic library of named lemmas: addition, multiplication and order; divisibility; binomial coefficients and the binomial theorem; division and remainder; powers and finite sums; primes and Euclid’s lemma; strong induction.

Language

  • let mut. A mutable binding can be reassigned, including inside branches. Reassigning an immutable one (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 is refused (E0094–E0096).
  • Resource handles are used once (E0092, E0093).
  • Packages. An albite.toml manifest lists local library folders, each used by name, with their own dependencies (E0120–E0124). A file’s sibling modules are found without an explicit path.
  • Text positions count bytes everywhere, so substring gives the same answer in the interpreter and in a compiled program.

Runtime

  • A compiled program sets up its own 512 MiB stack; ALBITE_STACK_SIZE changes it.
  • String joining, appending and argument reading are written in Albite itself, at the previous speed.
  • A compiled program carries only the runtime code it calls, and small sums are passed in registers.

Tooling

  • --error-format=json writes one versioned diagnostic record per line, for check, run and compile.
  • albite test --format json|junit, and albite test exits 0 (all passed), 1 (a test failed) or 2 (no verdicts).
  • Every syntax error and build failure has a code that albite explain error knows (E0110–E0117, E0140–E0146).
  • A test file beside its module — foo_test.tg next to foo.tg — joins that module when tests run.
  • albite check names the theorems that rest on an axiom or a sorry.

Fixed

  • ? inside a try block stops at the block, and compiles.
  • A return in statement position leaves the function in the bootstrap’s interpreter, as in compiled programs.
  • A full module path always runs the function it names, in the bootstrap’s interpreter too.
  • A compiled Nat division or remainder by zero gives zero, as the interpreter and the proof kernel do.

The full changelog, including the macOS self-hosted compiler’s own changes, is the repository’s CHANGELOG.md.

Still true

Every code sample in this manual was run through the beta.3 compiler, both the bootstrap and the macOS self-hosted one. Current limitations was re-checked against both, and lists where the two still disagree. The browser playground runs this release’s bootstrap compiler — see Installing Albite.