Overview

A pre-built binary, a container, or a build from source — and which parts need LLVM.

Why the language has a new name, what changed and what did not, and where the old addresses go.

Your first Albite program — type-checked, interpreted, then compiled to a native binary.

Functions, bindings, conditionals, pattern matching, data types and modules — enough Albite to read real code.

Literals, the built-in types, operators, blocks and the semicolon rule.

Declarations, the last-expression rule, early return, lambdas and function types.

if as an expression, match with exhaustiveness checking, nested patterns, if let and let else.

Sum types, records, field access, named constructors and record spread.

Type parameters on functions and types, how inference works, and generic type aliases.

Option and Result, the ? operator, and try blocks.

Declaring submodules, importing with use, visibility rules and import aliasing.

Declaring external C-ABI functions with extern "C" fn.

A type may refer to itself only to the right of an arrow. The compiler refuses the rest, with E0061.

Every recursive function must visibly stop. What E0062 means, and the three ways to satisfy it — including

A theorem may not depend on a

A type whose recursion passes through a generic parameter is accepted, but every match on it is refused with E0064. The fix is a non-generic intermediate type.

The Curry-Howard correspondence, and what it means for a program to be a proof.

The theorem keyword, proof by exhaustive checking, and where that technique stops working.

Types that depend on values, and what that buys — including where Albite's support currently stops.

The natind eliminator, motives, and proving something about every natural number.

A cheat-sheet for Albite's grammar — declarations, types, expressions and patterns.

The primitive types, the operator table, conversions, the conventional types and the reserved words.

The commands you need to write Albite — check, run, compile, test and explain.

What Albite cannot do yet, and where the two shipped compilers still disagree.

Write and run Albite in your browser.