Dependent
Types may state relationships among values, indices, representations, and evidence.
A language for evidence-bearing systems
Make the important boundary checkable.
Alpha is a dependently typed, quantitative systems language and sovereign compiler for programs whose semantics, resource use, effects, and native execution boundaries must stay explicit.
Active research software. Checked source is not automatically native or physically attested.
module Playground.Main
def identity : (pi unrestricted value : Nat . Nat) =
(lambda unrestricted value : Nat . value)
def main : Nat =
(app identity (succ zero)) reference normal form:
(nat-literal 1)- Source
- 7d4a2ac3
- Compiler
- 9b52594b00000000
- Edition
- alpha-2027
- REPL boundary
- checked + reference-evaluated
One language, four visible contracts
Alpha connects rich source terms to native artifacts without treating any intermediate milestone as proof of the next.
Quantitative
Erased, affine, linear, and unrestricted binders make runtime use part of checking.
Explicit
Effects and divergence remain visible in computation types.
Fail-closed
Unsupported native behavior is an error, never a silent host fallback.
Choose the question you have
The site keeps explanatory material, normative contracts, generated references, and project evidence distinct.
Learn the languageGuide →Syntax, types, quantities, effects, families, toolingEvaluate the fitStrengths and limits →Where Alpha earns its ceremony—and where it does notAudit a contractSpecification →Normative semantics and the trusted boundaryInterpret a claimEvidence status →Checked, emitted, self-hosted, physically attested