Where Does the Error Land?

The further the error fires, the longer the loop back. Static typing keeps that loop tight.

Dynamic Python / JS

parse

load

run

!

AttributeError

3 frames deep

loop back · minutes · redeploy

Static AILANG

parse

!

type error

line 12, col 4

tight loop · ~1s

compile time runtime

AILANG catches it at the gate. Python only knows once it's inside — and the fix loop pays for it. tight fix loop

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.

Neurosymbolic

AI writes the code. Z3 proves it.

AILANG — Contracts

-- ✓ 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 }

Neural

LLM writes AILANG with requires / ensures

Symbolic

Z3 SMT solver proves the contract for all inputs

Fix

Counterexample tells the AI exactly what to repair

This is neurosymbolic programming — coupled, on purpose. The neural side writes the code. The symbolic side proves it. No tests, no sampling — the solver reasons about every possible execution and hands back a concrete counterexample when it can't.

Code the AI Can Hold in One Context

No loops. Only pattern matching. Every branch is on screen — no mutable loop state to remember.

            
            Python
          
total = 0
for item in items:
    if item.active:
        total += item.value

            
            AILANG
          

pure func total(xs: List[Item]) -> int {
  match xs {
    [] => 0,
    ::(x, rest) =>
      if x.active then x.value + total(rest)
      else total(rest)
  }
}
          

Every branch is local. The model doesn't have to track an accumulator across loop iterations or wonder if it terminates. Compiler-checked exhaustiveness means fewer tokens spent on reasoning about state — and a one-turn fix when a branch is missing.

What's in Scope Is What's on Screen

The same line of code — two very different mental loads on the AI.

One line. What's in scope?

Python

import requests

what the AI must reason about

requests.get requests.post urllib3.* charset_normalizer idna certifi.* ssl socket http.client json os.environ logging warnings io.BytesIO … and more, transitively

2 named · 12+ reachable through the package

The model spends tokens guessing what else is in scope. Sometimes it hallucinates symbols that don't exist; sometimes it uses ones that do but it shouldn't.

One line. What's in scope?

AILANG

import std/net (get, post)

what the AI must reason about

get post

2 named · 2 reachable

The file is the inventory. Nothing arrives transitively. Whatever the AI cannot name, it cannot call.

Complexity Is in the Eye of the Beholder

Every AILANG choice has two readers. Same code — two very different reactions.

The Design Choice

Humangrumbles

AI Agentthanks you

Static, fully-inferred types

"Why annotate?"

Pre-runtime, parseable errors

No loops, only recursion

"Verbose"

Total, analysable iteration

Explicit effects in types

"Noisy signatures"

Can't hallucinate capabilities

No transitive imports

"Tedious"

Bounded context window

No mutable state

"Inconvenient"

No temporal reasoning needed

One canonical syntax

"Less expressive"

Zero ambiguity

Structured errors

"More boilerplate"

Parseable feedback for self-repair

7 complaints · Same language. · 7 wins