Read Alpha at the right level.

A ten-minute path from source to a checked result.

The comprehensive explanatory tour maintained with Alpha.

Indexed data, constructors, motives, recursion, and exhaustive elimination.

What Alpha is good at, what it is bad at, and the central tradeoff.

Primary literature behind dependent, quantitative, effectful, and verified programming.

How to read checked, self-hosted, and physically attested claims.

The normative language semantics and trusted boundary.

Generated concrete syntax and parser-facing forms.

Exact forms, quantities, effects, interfaces, and artifacts.

Stable error codes, phases, and repair guidance.

The public stable edition manifest.

The repository-selected draft edition manifest.

Application syntax, grouping, associativity, and diagnostics.

Bounded byte construction and runtime image building.

Path representation and file-effect boundaries.

Cache identity, invalidation, and verification.