XIOMWHY

Software fails between intent and enforcement

A programmer knows things about their code that the language never records:

• a value must never be negative
• an input must not be zero
• a collection must be sorted
• ownership must stay exclusive
• an invariant must hold
• an unsafe operation must stay inside a controlled boundary

If those requirements live only in comments, tickets or someone's memory, the compiler cannot enforce them. XIOM moves important intent into the language, where machines can check it.

The bottleneck is changing

Generating code is getting cheaper. Reviewing every line is not. A language built for that world has to do more than accept valid syntax -- it has to make important assumptions explicit and machine-checkable.

The model can generate the code. The language should enforce the boundaries.

We test this directly: the project runs a reproducible Docker benchmark that records generated source, compiler output, runtime behavior, tool usage, token usage and complete sessions. Results will be published together with the harness so anyone can rerun them.

From code to intent

fn div_exact(a: Int, b: Int) -> Int
    requires: b != 0 && a % b == 0
    ensures: result * b == a
{
    return a / b;
}

The function no longer merely contains an implementation; it states how it may be called and what it guarantees. Contracts are part of the program -- enforced at runtime today, and translated into verification obligations for supported properties where the tooling applies.

Four layers of protection

1. Language safety. Ownership and types reject whole classes of invalid programs: ownership violations, invalid borrows, missing error handling, null in safe code, non-exhaustive matches.
2. Contracts. requires:, ensures: and invariant: express properties that type checking alone cannot describe.
3. Verification. Where supported, XIOM translates contracts into verification obligations for solver tooling -- a different mechanism from a runtime check, and labelled as such. A contract in the source is not by itself a proof that it always holds.
4. Runtime containment. Raw pointers, FFI and inline assembly sit behind an explicit unsafe boundary; the toolchain audits those blocks, and the runtime can confine them.

Why this matters for AI

A language does not need to teach a model every rule in advance. It needs to make the rules difficult to violate silently. The loop becomes generate, compile, check, diagnose, repair, verify, run -- with the compiler inside the feedback cycle.

One language, from script to system

Use it as a script with xiom run. Iterate through the JIT. Move eligible computation to compile time with comptime. Compile to native machine code through LLVM, or to WebAssembly. The execution mode changes the workflow, not the language.

What XIOM optimizes

Not one number. The goal is a combination: safety, reliability, explicit intent, predictable behavior and practical performance -- a trade-off that matters more as more software is written with AI.

The design has costs, and they are documented: what XIOM gives up against Rust's lifetime system, where the contract ideas come from, and how runtime checks are paid for. See Prior art and trade-offs.

What XIOM is not

• Not a promise that every property is formally proven -- contracts are runtime-checked today, with verification tooling for supported properties.
• Not a language that removes unsafe operations -- it puts them behind a visible boundary.
• Not a guarantee that compiling code is free of logical bugs.
• Not finished -- this page describes intent; the language and toolchain are being built.

The philosophy

Safe. Intentional. Precise. Verifiable.

Safe

Ordinary code stays inside language-level guarantees: no garbage collector, no null in safe code, bounds and overflow protection, and explicit unsafe boundaries. Allocation is explicit in the language model, and library operations document when they allocate.

Verifiable

Contracts are part of the language, not the documentation: enforced at runtime today, and available to verification tooling for supported properties. Runtime checking and proof are different mechanisms, and are labelled separately.

Precise

Canonical syntax and explicit semantics: no implicit behaviour, no hidden control flow. The formatter enforces the single style, and derive handles the boilerplate.