the language · self-hosting · corpus-gated

Autodiff is a keyword. The compiler is the proof.

Helix is a source-available, fully auditable, from-scratch self-hosting language for ML and high-certainty systems work. Its compiler, kovc — complete lexer, parser, and x86-64-ELF code generator, written in Helix (helixc/bootstrap/{lexer,parser,kovc}.hx) — is built from the raw seed into a native binary that compiles Helix programs, including its own source. It emits self-contained Linux x86-64 ELFs directly: no assembler, no linker, no libc.

Get started → See the verified run
Differentiation, built in

Gradients are a language feature, not a library.

Source-level forward- and reverse-mode autodiff as built-ins: grad, grad_rev, grad_rev_all. Chain rules compose across user-defined functions via inlining and across stdlib transcendentals via analytic rules.

autodiff.hx · grad_rev_all 
fn loss(x: f64, y: f64) -> f64 {
    x * y + x * x
}

struct Grad { dx: f64, dy: f64 }

fn main() -> f64 {
    // reverse-mode AD, all gradients in one sweep
    let g = grad_rev_all(loss)(2.0_f64, 3.0_f64);
    g.dx
}
kovc loss.hx -O2 → 7.0_f64

Everything is lowered at compile time — no runtime tape, no tracing. The derivative of your program is just more of your program, compiled by the same gated compiler into the same self-contained binary.

Shapes & silicon

Dimension bugs die at compile time.

Tensor shapes are Presburger-checked: a mismatched matmul is a compile error, not a wrong number at runtime. The same compiler then emits PTX that runs on real NVIDIA GPUs.

matmul.hx · compile-time shapes 
fn main() -> f32 {
    let a = tile<f32, [4, 4], REG>::ones();
    let b = tile<f32, [4, 4], REG>::ones();
    let c = tile_matmul(a, b);
    c.get(2, 3)
}
tiles · Presburger-checked shapes → 4.0_f32

kovc emits PTX for a covered transformer-kernel set, and every kernel is gated for numerical parity against an independent oracle before it counts as covered. This is the kernel set that runs GPT-2 and SmolLM2 token-for-token against that oracle.

matmul attention softmax layernorm RMSNorm RoPE SwiGLU activations
Controlled power

Self-modifying code, behind your own verifier.

Reflection in Helix is not a trapdoor. quote / splice_f / modify_f call your verifier function before committing any mutation — 64 mutable cells in the binary's writable region, and nothing changes unless your check passes.

reflect.hx · verifier-gated 
fn always_true(_: i32) -> i32 { 1 }

fn main() -> i32 {
    let h = Quote(0);
    modify(h, 42, always_true(0));
    Splice(h)
}
reflection · your verifier decides → 42

Effects get the same treatment at the other end: @pure functions are verified at the IR level and transitively prohibited from reaching effectful code. Purity is a checked property, not a comment.

The gated surface

If it's listed here, a gate enforces it.

Every kovc build passes scripts/gate_kovc.sh: the self-host fixpoint, the 109-program feature corpus, 4 negative-diagnostic checks, and the PTX regression.

feature corpus 109 programs negative-diagnostic checks 4 stdlib 16 modules stdlib functions ~455 self-host fixpoint K2 == K3 == K4
Area In the language today
numerics Integer widths; floats including bf16/f16 arithmetic.
control & functions Control flow; closures, including capture-by-value.
types Generics; traits with default methods; pattern matching; wide struct fields.
autodiff grad, grad_rev, grad_rev_all — lowered at compile time, no runtime tape.
effects & reflection @pure verified at the IR level; quote / splice_f / modify_f gated by your verifier.
research types Presburger-checked tensor shapes; confidence types D<T>; memory-tier types; agent types — all checked at compile time.
gpu PTX for the covered transformer-kernel set, each kernel parity-gated against an independent oracle.
diagnostics Structured path:line:col diagnostics, held to the negative-diagnostic checks.
stdlib 16 modules, ~455 functions: math with range-reduced transcendentals; activations (sigmoid/tanh/silu/gelu/softplus/relu); losses (mse/mae/bce/huber); PRNG; optimizer steps; reverse-AD helpers; hashmap; tensor/iterator/vec/string/result helpers.
Proof it does ML

Real programs, in Helix-emitted binaries.

Not slideware — these compile with the seed-minted kovc and run as self-contained ELFs.

  1. One-parameter gradient descent. The smallest honest training loop: a single weight, a real gradient, a converging loss.
  2. Linear regression. Fit by compiled autodiff, not by a framework.
  3. An affine fit. Weight and bias learned together through the same compile-time-lowered gradients.
  4. A 2-layer ReLU XOR net. The classic nonlinearity test, end to end in Helix.
  5. Logistic regression. Sigmoid + BCE with multi-output autodiff across the whole model.
  6. A flagship agent. Composes everything above — autodiff, tiles, effects, reflection — in one program.

Documented bounds, loud failures

Helix states its design bounds instead of hiding them: borrows, const/static, module privacy, and match exhaustiveness are documented design bounds, not enforced checks. And when something goes wrong at runtime, it fails loudly with trap ids — never silently.

Getting started

Mint your own compiler first. Then write code.

One committed command rebuilds the whole ladder from the 299-byte root and proves the fixpoint — clean checkout, CPU-only, about a minute. Linux or WSL2.

terminal · linux / wsl2 
# rebuild the toolchain from the 299-byte root
git clone https://github.com/Questeria/helix
cd helix
bash scripts/reproduce_trust.sh
# builds the ladder + proves the fixpoint
# clean checkout · CPU-only · ~1 min

# the universal gate: fixpoint + 109-program corpus
# + 4 negative-diagnostic checks + PTX regression
bash scripts/gate_kovc.sh
gcc — only as the independent DDC auditor GPU (CUDA, RTX-class) — only for the GPU legs

After that, the seed-minted kovc compiles your .hx directly to a Linux x86-64 ELF — no assembler, no linker, no libc, and no Python anywhere in the toolchain. The repo carries exactly one committed .py file: a fenced numpy verification oracle that is never on the compile or run path.

No pre-built compiler is ever trusted: the ladder runs hex0 → hex1 → hex2 → catm → M0 → cc_amd64 → M2-Planet → seed → kovc, each rung built only by the rung before it.

Start here

Quickstart

From clone to your first compiled Helix binary, in order, with nothing assumed.

QUICKSTART.md → Learn the language

Tutorial

A guided tour of the surface: numerics, control flow, traits, closures, autodiff.

docs/lang/tutorial.md → The reference

Language spec

The precise definition of what the corpus-gated language surface means.

docs/lang/spec.md → Everything in one place

Full reference

The complete reference: language, stdlib modules, built-ins, diagnostics.

HELIX_REFERENCE.md → Trust, hands-on

Clean reproduction

Rebuild everything from a clean checkout and check the hashes yourself.

docs/CLEAN_REPRODUCTION.md → The source

GitHub repository

Every byte of the toolchain, from the hand-authored root to the PTX it emits.

github.com/Questeria/helix →
From keyword to kernel

A language you can audit to the last byte.

The compiler that lowers your gradients was itself built from 299 hand-authored bytes — and the models it runs were verified token-for-token against an independent reference.

See the verified run → Reproduce the chain