Can I Control What It's Allowed To Do?
Axiom 3
Effects Are Real and Legible
"Effects define what a computation is allowed to do, not just what it computes."
Axiom 4
Authority Must Be Explicit
"Ambient authority is treated as a design error."
Axiom 9
Cost Is Part of Meaning
"Programs should make their resource implications visible to tools and agents."
Axiom 12
The Language Is a System Boundary
"Crossing that boundary must always be explicit."
AI Cannot Hallucinate a Network Call
export func process(path: string) -> string ! {IO @limit=3, FS}
IO
—
Can print to console
@limit=3
—
Maximum 3 times
FS
—
Can read/write files
No Net
—
CANNOT touch the network
No DB
—
CANNOT access a database
$ ailang run --caps IO,FS process.ail
Only IO and FS granted at runtime. Attempting Net or DB → immediate rejection.
Pure Functions Enable Mathematical Proof
-- ✓ This one verifies
export func calculateTax(income: int) -> int ! {}
requires { income >= 0 }
ensures { result >= 0 }
{ income / 5 }
-- ✗ Subtle bug: what if price < discount?
export func applyDiscount(price: int, discount: int) -> int ! {}
requires { price >= 0, discount >= 0 }
ensures { result >= 0 }
{ price - discount }
$ ailang verify --verbose billing.ail
VERIFIED calculateTax 6ms
VIOLATION applyDiscount
Counterexample:
price: Int = 0
discount: Int = 1
-- 0 - 1 = -1, violates ensures { result >= 0 }
Z3 proves contracts correct for all inputs — not just test cases. Pure functions + no side effects = the SMT solver can reason about every possible execution. A one-turn fix: the counterexample tells AI exactly what's wrong.
No Loops. Only Pattern Matching.
total = 0
for item in items:
if item.active:
total += item.value
pure func total(xs: List[Item]) -> int {
match xs {
[] => 0,
::(x, rest) =>
if x.active then x.value + total(rest)
else total(rest)
}
}
Total, analysable iteration. No hidden termination conditions. The compiler verifies exhaustiveness — every case must be handled. One-turn fix when a branch is missing.
Imports Are Never Transitive
module myapp/handler
import std/io (println) -- only println, nothing else
import std/fs (readFile) -- explicit: just readFile
-- std/net not imported → Net effect DENIED by compiler
Python / JavaScript
import foo gives you everything foo imported. Three levels deep, you're using symbols you never asked for.
AILANG
Every symbol is explicitly requested. No transitive leakage. AI can't use what wasn't granted.
Complexity Is Relative to the Reader
No loops, only recursion
"Verbose"
Total, analysable iteration
Explicit effects in types
"Noisy signatures"
Can't hallucinate capabilities
No transitive imports
"Tedious"
No scope confusion
No mutable state
"Inconvenient"
No temporal reasoning needed
One canonical syntax
"Less expressive"
Zero ambiguity
Structured errors
"More boilerplate"
Parseable feedback for self-repair