"Why Vox: Compiler-Verified AI Code"

Why Vox: Compiler-Verified AI Code

The primary barrier to AI-driven software engineering is not the model's intelligence, but the hallucination boundary of current languages.

1. The Python Problem

When an LLM generates Python code (FastAPI, SQLAlchemy, etc.), it is guessing across a massive, unconstrained state space:

  • Runtime Persistence: Did it guess the correct column name?
  • Dependency Drift: Is that library version actually installed?
  • Dynamic Typing: Will this None propagate into a crash 5 minutes into execution?

In Python, the feedback loop is runtime failure. The model has to run the code, see the crash, and attempt a second guess. This is inefficient and risky for autonomous agents.

2. The Vox Solution: Compiler-Enforced Reality

Vox is designed so that the compiler acts as the guardrail for the LLM.

@table: The Database is the Source of Truth

In Vox, you don't write SQL strings or use a loose ORM. You define your schema with @table.

fn demo_scalars() {
    let i: int = 42
    let f: float = 3.14
    let s: str = "hello"
    let b: bool = true
    let c: char = 'x'
}

// vox:skip
@table type User {
    email: str
    points: int
}

If an LLM attempts to generate code that accesses user.score instead of user.points, the Vox compiler fails immediately. The model receives a precise type error: Field 'score' not found on type 'User'.

Zero-Null Discipline

LLMs frequently forget to check for null. In Vox, null does not exist. You must handle Option[T] using match.

fn handle_state(net_state: NetworkState) {
    match net_state {
        Disconnected -> print("offline")
        Connecting -> print("connecting...")
        Connected(address, port) -> print("connected to " + address)
    }
}

If the LLM omits the None case, the compiler rejects the code for a non-exhaustive match. The model is forced to be correct.

3. Results: Practical Implications

By constraining the LLM's output to a strictly-typed, compiler-verified grammar:

  • The compiler provides exact field-name errors rather than runtime stack traces, reducing the iteration cycle for LLM-driven code generation.
  • Lower K-Complexity: A single .vox file replaces 10+ files of boilerplate across Rust and TypeScript.

Next Steps: