How the Alpha language and compiler work

Alpha connects a high-level statement of meaning to native work without pretending that the steps in between are interchangeable. The language describes programs, proofs, resource use, and effects. The compiler checks those claims, erases what is static, lowers the remaining work through typed intermediate forms, emits native artifacts, and records what was actually established.

The short version

.alpha bytes
  -> lossless source and concrete syntax tree
  -> modules and resolved names
  -> elaborated dependent core
  -> trusted type / quantity / effect / totality checking
  -> checked interfaces and a sealed program
  -> proof- and type-directed erasure
  -> semantic IR and explicit control flow
  -> schedule, memory, and target-specific lowering
  -> x86-64 / SM86 instructions, objects, ELF, and device work
  -> certificates, identities, telemetry, and physical receipts

The detailed host pipeline is documented in Compiler pipeline, Compiler architecture, and Core and IR.

The language: meaning first

Dependent types

Types may depend on values. That lets an API state relationships that ordinary type systems leave to comments or runtime checks: a result has the same length as an input, a tile belongs to a particular shape, an index is within a finite axis, or a hardware plan satisfies a requirement.

Dependent types do not automatically prove that every program is correct. They provide a language in which a contract can be stated and checked at the boundary where it matters.

Quantitative use

Binders carry one of four usage quantities:

This makes ownership and runtime relevance part of checking. A linear buffer used twice is a type error, not a warning discovered after code generation.

Explicit effects and divergence

Computation types expose effects rather than hiding them behind ordinary function syntax. File access, process behavior, or other observable work remains part of the term the checker sees. Totality and possible divergence are also tracked rather than assumed away.

Families, constructors, and elimination

Alpha's family declarations define indexed data. Constructors say how inhabitants are formed. Elimination says how every possible constructor is consumed while respecting the indices and motive. This single mechanism supports booleans, naturals, options, vectors, proofs, and richer protocol state.

See Families and branches for the practical explanation.

Why there is no primitive if

if is not missing as a capability. It is derived from data and elimination.

A Boolean-like family has constructors such as true and false. Matching or eliminating that value supplies one branch for each constructor. The compiler can then lower the result to a direct conditional branch when a runtime decision remains.

That design avoids making one built-in branching form special. The same checked machinery handles:

• two-way Boolean choice;
• optional values;
• recursive naturals and lists;
• indexed states where each branch refines what is known; and
• user-defined data the compiler authors did not anticipate.

At the machine level, Alpha absolutely has branches, conditionals, loops, and jumps. The claim is only that source-level choice comes from exhaustive elimination rather than an unrelated primitive.

The deeper goal: put each decision in the right phase

The absence of a primitive source-level if is not mainly an attempt to make programs look branchless. The more important goal is to distinguish three kinds of choice:

Conventional training programs often express all three with ordinary booleans and integer fields. The result is a web of runtime if statements whose combinations determine shapes, memory, kernels, and even semantics.

Alpha's intended post-elaboration representations do not allow a target-name string or an unchecked boolean to select semantics. Exact shapes, layouts, address spaces, ownership, numerical contracts, target capabilities, resource use, and synchronization state must travel through typed compiler representations.

When a choice is closed at compile time, normalization and specialization should resolve it. The compiler lowers only the selected branch, computes its resource consequences, and erases the configuration evidence that the machine no longer needs. A target-specific ELF should therefore contain the path for its exact experiment, not a general dispatcher that asks the same configuration questions on every training step.

When a choice is dynamic, elimination still makes the cases explicit and exhaustive. It survives into typed control flow and eventually a machine branch. Alpha does not erase real uncertainty; it tries to prevent static uncertainty from leaking into runtime.

Hyperparameters participate in types and plans

A hyperparameter is not always “just a number.” Depending on its role, it may affect different compiler layers:

Some values naturally index types. Others are checked constants carried by a validated plan. The design does not require forcing every scalar into a type merely for appearance. It requires every value whose change can invalidate shapes, resources, semantics, or an artifact identity to be visible to the compiler before promotion.

The desired failure mode is therefore a compile-time explanation such as “this realization needs more shared memory than this target profile provides,” not a runtime out-of-memory event or a hidden CPU fallback.

See Learning systems: the conditional-explosion problem for the model-training view.

One engine, many tools

The formatter, linter, language server, REPL, documentation generator, test runner, and inspector use the same language engine. They do not each carry an approximate parser or a second idea of name resolution.

The source model is lossless: comments, whitespace, and malformed regions remain represented in the concrete syntax tree. That lets editor tools preserve source faithfully while the semantic pipeline operates on resolved modules and checked terms.

The engine also provides structural queries such as symbols, references, forms, outlines, and typed control-flow inspection. That matters to agents: a refactor should be based on resolved identity, not a search result that happens to contain the same spelling.

The trusted kernel

Elaboration converts convenient surface syntax into a smaller core language. It may resolve names and construct candidate terms, but it may not declare them valid.

The trusted kernel owns:

• type inference and checking;
• definitional equality and normalization;
• quantitative usage accounting;
• effect rows;
• positivity and totality; and
• proof- and type-directed erasure boundaries.

Downstream stages accept a CheckedTerm, not an unchecked promise. A cache may re-admit checked information only through validated interfaces with bound digests.

Core says what; IR says how

Alpha deliberately uses more than one internal language.

Core answers: “What does this program mean, and is the claim well formed?” It is expressive enough for dependent types, proofs, quantities, and effects.

Semantic IR answers: “What work must a machine perform?” It projects the runtime-relevant portion into a smaller typed language, then defunctionalizes closures and lowers decisions and iteration into typed control flow.

This separation prevents a backend from carrying a general dependent interpreter merely because the source language is rich. Compile-time evidence can disappear; runtime work becomes explicit.

Erasure is an architectural boundary

Proofs, types, and erased arguments guide acceptance but should not consume runtime space or cycles. Erasure removes them only after the trusted checker has used them.

The important property is not “proofs are free” in the abstract. It is that a named compiler phase, operating on checked terms, decides what has no runtime relevance. The remaining program must preserve observable meaning.

Two host emission lanes

The current compiler documents two host lanes:

The direct lane interprets its lowered control flow and compares it with the preceding residual when a compile-time answer exists. It also decodes and re-encodes emitted x86 instructions. Programs that read runtime files cannot have their result value compared at compile time; the certificate records that limitation instead of inventing an input.

Learning-system lowering

For learning workloads, the broader architecture continues below ordinary host control flow:

checked learning program
  -> model, learning, and operator semantics
  -> selected realizations
  -> validated schedule and static memory plan
  -> target capability and resource checks
  -> host control path + accelerator machine work
  -> instruction encoding, device image, launch protocol, and ELF

The completed RTX 3070 milestone demonstrates that the compiler can lower the tiny Transformer's training computation from .alpha through native SM86 without Python-generated math kernels or a host fallback. It does not mean every model, learning rule, shape, target, or optimization has a mature lowering.

“From scratch” has a precise boundary

Alpha owns unusually deep layers: the language, checker, compiler representations, instruction encoders, ELF construction, SM86 compute lowering, GPU command and launch machinery, training path, checkpoints, and evidence artifacts are project-authored.

It still has an external floor. The current developer compiler is bootstrapped through Haskell/GHC, and physical runs rely on the Linux kernel, NVIDIA kernel module and firmware, CPU/GPU silicon, storage, and networking. Current-generation self-hosting is a separate gate. “Built from scratch” means Alpha is not a wrapper around PyTorch, CUDA, LLVM, or a vendor training runtime; it does not mean the project claims to have fabricated the operating system and hardware beneath it.

Fail closed, then explain

An unsupported form, missing lowering, target mismatch, resource overflow, stale cache entry, or unresolved relocation is supposed to stop with a stable diagnostic. The compiler must not quietly execute the operation in the bootstrap host or substitute a different target.

That can make Alpha less convenient than a framework that always finds a way to run. It is also what makes an experiment interpretable: success says something precise about the path that was exercised.

The evidence ladder

The compiler's product is not a single green badge. Alpha distinguishes declared, source-present, checked, tested, emitted, self-hosted, physically attested, and quality-bearing claims. See Evidence and status before interpreting any milestone.

Read next

• How learning systems are expected to work
• The philosophy behind Alpha
• Language guide
• Specification