The Axiom mental model
The biggest change is not syntax. You write both what should happen and the conditions that make it valid.
Normal programs contain invisible assumptions: an index is in range, a buffer is large enough, a task is done, a reference is still alive. Axiom tries to turn those assumptions into facts the compiler can see.
The one-sentence rule
An API without “might crash”
1first_byte(view<const u8> data) -> u8:2 require data.size() > 03 RETURN data[0]45main -> u8:6 const u8 packet[] = { 0x41, 0x58 }7 view<const u8> bytes = packet8 RETURN first_byte(bytes)A borrowed view replaces raw pointer + length.
The caller must prove the view is non-empty.
Index zero is then proven safe.
The array lives for the whole main scope.
The view borrows that storage.
Its size is two, so the call is valid.
Not just another assert
require does not mean “check at runtime and abort”. It is a proof obligation. If the compiler cannot prove it, compilation fails. If you intentionally need a runtime check, use runtime_assert.
Determinism means resources too
Axiom uses determinism broadly: predictable memory, explicit lifetimes, analyzable task effects, stable lowering, and no hidden allocation. “It works” is weaker than “we know why it is valid and how much it can consume”.
What “sus” means
sus is project slang for a trusted or insufficiently proven boundary: MMIO, external assembly, or a manual assume. It is not necessarily forbidden; it simply must not look like ordinary safe Axiom code.