Research language · edition alpha-2027 (draft)

Compile a learning system, from its mathematics to its GPU instructions.

Alpha is a dependently typed language and compiler. It checks a model, its learner and its hardware pairing as one program, then emits every byte of a self-contained executable: host code, GPU code, launch tables and memory plan.

Get started Try it in the browser GitHub

Hello.alphaalpha-2027

module Hello

def double : (pi unrestricted n : Nat . Nat) =
  (lambda unrestricted n : Nat . (nat-add n n))

def main : Nat =
  (double 21)

alpha run → exit status 42 · a 29 KB static x86-64 ELF

35,683tokens/sCoppelius training on an RTX 30901.51× PyTorch with CUDA graphs and 2.35× eager PyTorch, in matched 2,000-step runs from the same checkpoint (27 Sep 2026).10,000stepsOne uninterrupted training run57.7M parameters on the RTX 3090 with ten checkpoints, every loss finite, then resumed in a fresh process.2GPU architecturesFrom one model sourceAmpere (sm_86: RTX 3070, 3090) and Blackwell (sm_121: DGX Spark GB10). Only the device pairing changes.0vendor runtimesBetween the program and the driverNo CUDA, no PyTorch, no libc. The executable issues its own driver calls, launches and memory mappings.

01
Describe
Write the model, the learner, the run policy and the target device as ordinary Alpha definitions: one closure, no configuration files.
02
Check
Dependent types, quantities and effects are checked across the whole closure. Shapes, layouts and resource limits are facts, not comments.
03
Realize
The compiler plans memory, schedules launches and lowers kernels to GPU machine code, and refuses any image that fails its hazard check.
04
Run
One static ELF trains, checkpoints and predicts. Runs are recorded as observation streams, so claims can cite what happened.

Dependent types: Types can mention values, so a tile that does not fit shared memory, or a buffer of the wrong length, is a type error.
Quantities: Every binder is erased, affine, linear or unrestricted. Proofs and type-level data vanish from the executable by construction.
Explicit effects: Effects and partiality are part of a computation's type. Nothing performs I/O or diverges without saying so.
No fallbacks: If a target cannot do something, compilation stops with a stable diagnostic. Work never silently moves to the host.

Stable diagnostics. Errors carry stable codes and point at the exact source span; catalogued codes come with a repair.
Machine-readable everything. Receipts, observation streams and inventories are JSON with schemas.
Checked results, untrusted producers. Schedulers and allocators can be rewritten freely; their output is still checked.
Evidence, not assertions. A claim about speed or loss cites the recorded run behind it.

LearnGetting started

Build the compiler and run a first program.

LearnLanguage guide

Syntax, types, quantities, effects and families, with examples.

ExploreLearning systems

The models Alpha compiles and what each has run on.

ExploreHardware

Every target device, its typed profile and what is measured on it.

ExploreTraining runs

Live dashboards for runs on the RTX 3090 and the DGX Spark.

ExploreSource browser

Every Alpha file, with definitions linked across modules.