Language design · Compilers · AI-native

Sigil

A prototype AI-native programming language — capability-secure, effect-typed, and contract-carrying. Designed to be written by AI and audited by humans, and compiled to native code.

Why a new language

As more code is written by AI, the bottleneck shifts from typing to trusting. Sigil is an experiment in a language whose guarantees are strong enough that AI-generated code can be reviewed with confidence: authority is explicit, side effects are visible in the type signature, and behavioral contracts are checked — proven away at compile time where possible. Write it by machine; audit it by human.

fn safe_div(a: Int, b: Int) -> Int
    requires b != 0
{
    return a / b;
}

fn main(console: Console) -> Unit ! {io.write} {
    print(console, "10 / 3 = " + str(safe_div(10, 3)));
}

The three core ideas

1 — No ambient authority

Side effects require an unforgeable capability value, handed down from main. A dependency you never gave the filesystem to cannot touch it — there's no global open() to reach for. Capabilities attenuate: read_only(subdir(fs, "sandbox")) mints a strictly weaker capability to pass to code you trust less.

2 — Effects in the type

Every function declares what it may do — ! {io.write} — and undeclared effects are compile errors. No annotation means the function is provably pure. The effect a function can have is part of its contract with the caller, not a hidden surprise.

3 — Contracts with blame, proven where possible

requires/ensures on functions and invariant on loops. When a contract is violated, the error names the guilty party — caller, callee, or loop. With the z3-solver installed, sigil verify proves clauses statically (recursion inductively, loops via invariants), and sigil build erases every proven runtime check from the binary. Clauses it can't prove conservatively stay as runtime checks.

The rest of the language

• Records — record Point { x: Int, y: Int }.
• Sum types with exhaustive match — enum Shape { Circle(Int), Empty }; a missing variant is a compile error, and so is a dead arm.
• Generics — fn first[T](xs: List[T]) -> T, monomorphized to native code.