Axiom · light
From Axiom to Ada and SPARK
After Axiom, many “strange” Ada ideas stop looking strange: ranges, contracts, strong types, and proof-oriented design all reduce accidental states.
Axiom does not copy Ada syntax. It tries to teach the same engineering reflex: define the valid state first, then implement the operation.
| Axiom | Ada/SPARK idea | Shared purpose |
|---|---|---|
require | Precondition | Caller obligation |
ensure | Postcondition | Callee obligation |
invariant | Type/Loop invariant | Preserved property |
| bounded values/contracts | Range/subtype constraints | Reject invalid values early |
view + lifetime proof | accessibility/ownership discipline | Prevent dangling references |
| no recursion + memory reports | high-integrity resource reasoning | Bound stack/resources |
| proof reports | GNATprove-style analysis | Diagnostics as proofs, not only warnings |
A small design-by-contract example
Design by contractAxiom
1percentage(i32 value) -> i32:2 require value >= 03 require value <= 1004 ensure result >= 05 ensure result <= 1006 RETURN value1
The raw integer type is wider than the domain concept.
2
Preconditions narrow the valid domain.
4
Postconditions export a guarantee to future callers.
6
The body is trivial; the contract carries the semantic knowledge.
What to notice when you open Ada/SPARK
Focus on subtypes/ranges, contracts, tasking, strong typing, accessibility rules, and GNATprove. Those are practical tools for software where “usually works” is not an acceptable requirement.