Start here
Axiom for programmers who already know how to build software, but do not want to become experts in undefined behavior, ABIs, and theorem proving just to get predictable systems.
Axiom is a strongly typed systems language where the compiler tries to prove that an operation is valid before the program runs. The goal is not to bury you in proofs. The goal is to make dangerous states awkward or impossible to express.
CONTINUE and parts of the standard library are documented as planned standard surface.For web developers
Think of Axiom as the “do not let me do something stupid” instinct of a typed web stack extended all the way down to memory, threads, and hardware.
For systems code
No exceptions, no ordinary raw-pointer programming, no hidden general heap, and no unproven shared mutable state.
For embedded
The compiler can reason about memory upper bounds, scratch lifetimes, and CPU capabilities.
Your first program
1discounted_total(i64 price, i64 percent) -> i64:2 require price >= 03 require percent >= 04 require percent <= 1005 RETURN price - (price * percent / 100)67main -> i64:8 RETURN discounted_total(1250, 20)A function declaration: explicit parameter types and return type.
require is a caller obligation, not a comment.
The lower bound is part of the function contract.
So is the upper bound.
A normal arithmetic expression; proven facts may remove redundant runtime checks.
A parameterless main.
All arguments are compile-time constants here, so the requirements are trivial to prove.
What Axiom deliberately avoids
Axiom is not C++ with a different spelling. It avoids exceptions, RTTI, ordinary raw-pointer APIs, silent data races, recursion, and “hopefully this buffer is large enough”. When a hardware or ABI boundary is inherently unsafe, that code is kept short, explicit, and marked as sus.
How to read this documentation
Read “Mental model” → “Contracts” → “Views” → “Deterministic memory” first. The syntax will make much more sense afterwards. Then move into compiler, targets, and hardware to see how those guarantees survive lowering to ABI and machine code.