Evidence and status#
Alpha deliberately separates claims that software projects often collapse. A source file, a green checker, a generated executable, and a physical run are different facts.
Assurance ladder#
| Level | What it establishes | What it does not establish |
|---|---|---|
| Declared | A contract or requirement exists. | An implementation exists. |
| Source present | Relevant implementation text exists. | It parses or checks. |
| Checked | A named compiler identity accepted the relevant closure. | Native lowering or execution works. |
| Tested | A named test ran against named source and tool identities. | Every target or environment is covered. |
| Emitted | A target artifact and receipt were produced. | The artifact executed correctly. |
| Self-hosted | Bound compiler generations reproduced the required canonical identity. | A changed generation is also self-hosted. |
| Physically attested | A named machine executed a bound artifact and produced durable evidence. | General correctness outside that profile. |
| Quality-bearing | A separate empirical result supports performance or output quality. | Compiler proof obligations disappear. |
What alpha check proves#
For the selected workspace, root, edition, and compiler identity, a successful check establishes the implemented parsing, resolution, elaboration, trusted type/quantity/effect checking, and totality obligations for the closure. It does not establish that every checked term has a supported native lowering.
What the checked learning step proves (2026-09-22)#
One path now reaches a stronger fact than "checked": for a 2×2 linear model, Proof.CheckedLinearStep has the type checker decide, by definitional equality over the bit-exact binary32 model, that the 56 SASS instructions the realization emits — run on SM86.MachineModel, a model of one SM86 thread — write exactly the outputs, loss, gradient and updated weights the semantic program Learning.Checked.LinearStep specifies, with the arena placement certified (Runtime.ArenaCertificate). The build then realizes the plan into the device tables and refuses an unencodable instruction. Mutated kernels and overlapping arenas are refused (scripts/ci/checked-linear-step.sh, in CI). It establishes: the generated machine program implements the specified learning step on the model, and — after the RTX 3090 returned a record of zeros for the first realization (no scoreboard barriers on its loads; the functional model cannot see latency), which added the SM86.Scoreboard pass and the barriers — that the silicon's 44-byte record for the same instance is bit-identical to the specification (Proof.CheckedLinearStepSilicon). The executable that produced that record is built by the compiler from the plan — Platform.Linux.Nvidia.PlanHost derives the device-open, allocation, mapping, submission, fence and readback protocol from the plan's placement; no hand-written host, no Python — and it ran in 37–45 ms. It does not establish: anything beyond that one device, driver, shape and instance. Report: docs/language/prd/reports/R10-CHECKED-LINEAR-STEP-REPORT.md.
What the training runs establish (2026-09-27)#
Coppelius, a 57.7M-parameter transformer, trains from .alpha source on three physical devices: the RTX 3070, the RTX 3090 and the DGX Spark's GB10. On the RTX 3090 a 10,000-step run finished with every loss finite and resumed in a fresh process, and matched 2,000-step runs from one checkpoint measured Alpha at 35,683 tokens/s against 23,675 for PyTorch with CUDA graphs, with mean losses within 0.004 nats (record). On the GB10 the compiler lowers the same kernels to sm_121 and 10,000-step runs complete (record). These establish: those models train on those devices at those rates. They do not establish: identical parameter trajectories to PyTorch, results on other devices, or model quality beyond the recorded losses.
What this site's REPL proves#
The workbench runs the actual deployed Alpha binary in a sandbox. It checks one isolated module and reference-normalizes main. The result is useful language feedback, but it is intentionally labeled reference evaluation. The site does not claim native execution, GPU execution, checkpoint continuation, or current-generation self-hosting.
Current project boundary#
Alpha is an active bootstrap research project. Substantial language, checker, formatter, linter, LSP, x86-64 and AArch64, ELF, sm_86 and sm_121, GPU runtime, learning-system, and evidence machinery exists, and real models train on real hardware. The exact promoted state moves with the source, current release reports, and durable evidence directories rather than a timeless badge.
Documentation authority#
When sources disagree:
- the Specification defines normative language behavior;
- an edition manifest binds behavior to concrete schemas and artifacts;
- generated grammar, reference, and diagnostics describe their pinned implementation surface;
- the guide explains but does not override the specification; and
- the changelog records movement within an edition.
Generated pages include their own source revision. A historical generation header is not proof that every later repository change was re-audited.