A prompt is a request. A language is the law: Aver and AI-written code

I did not start Aver because I think AI changes everything.

I started it because, if AI is going to write more of our software, syntax is not the problem.

The problem is intent.

AI can already generate code that looks plausible. What it often fails to preserve is the information reviewers actually need: what a function is allowed to do, why a design was chosen, what behavior must not regress, and where side effects cross the boundary of the process.

That is why I built Aver, a statically typed language with a Rust interpreter and a Rust code generation path for deployment.

One line from the manifesto I wrote captures the philosophy better than any pitch:

A prompt is a request. A language is the law.

Most AI tooling wraps existing languages with better prompts, agents, and editors. When I started building Aver, I asked a different question:

What if the language itself changed once we assume AI writes a large share of the code?

Make intent part of the program

The core move in Aver is simple: stop treating intent, effects, tests, and design rationale as optional conventions spread across comments, wikis, ADR folders, and chat logs.

Make them part of the source.

In Aver:

• functions can carry a prose description with ?
• effects are part of the function signature
• pure behavior lives in colocated verify blocks
• architectural rationale can live in decision blocks next to the code it affects
• aver context can export a contract-level view of a module graph for humans or LLMs

This is the kind of code I wanted Aver to make natural:

type Cmd
    Burn(Int)
    Rotate(Int)
    DeploySolar
    Tick(Int)
    Abort

decision EffectsAtTheEdge
    date = "2026-03-02"
    reason =
        "State transition logic should be deterministic and testable with verify."
        "Console output belongs to the outer shell only."
        "Replay mode then captures behavior without mocking."
    chosen = "PureCoreEffectfulShell"
    rejected = ["PrintInsideCore", "GlobalMutableState"]
    impacts = [runPlan, main]

fn parseCommand(line: String) -> Result<Cmd, String>
    ? "Parse one command line: BURN n, ROTATE n, DEPLOY, TICK n, ABORT."
    clean = String.trim(line)
    match clean == ""
        true -> Result.Err("Empty command")
        false -> parseCommandTokens(String.split(clean, " "))

verify parseCommand
    parseCommand("BURN 12") => Result.Ok(Cmd.Burn(12))
    parseCommand("ABORT") => Result.Ok(Cmd.Abort)
    parseCommand("JUMP") => Result.Err("Unknown command: JUMP")

fn runMission(cmds: List<Cmd>) -> Unit
    ? "Effectful wrapper around pure runPlan."
    ! [Console.print]
    match runPlan(cmds)
        Result.Err(msg) -> Console.print("MISSION FAILED: " + msg)
        Result.Ok(state) -> reportMission(state)

That is the point of Aver in one screen.

You can see the rationale. You can see the pure part that gets verify. You can see the effect boundary where printing is allowed. You can see the architectural choice to keep the core deterministic and push I/O to the edge. You do not have to reconstruct that from a function body and three adjacent tools.

Design by inconvenience

I made Aver intentionally inconvenient to write by hand.

That is not an accidental rough edge. It is the strategy.

My bet is that AI generates the verbose version and humans review the explicit one.

So Aver removes a lot of familiar escape hatches:

• no if/else, only match
• no loops, use recursion and explicit list operations
• no exceptions, use Result
• no null, use Option
• no mutable bindings
• no closures or lambda-heavy style

If you optimize for author comfort, this looks hostile.

If you optimize for auditability, it starts to look coherent.

Closures hide capture. Exceptions hide control flow. Mutable state hides causality. Wide-open branching makes verification harder. That is why Aver ended up looking functionally constrained, but my argument is not "FP is elegant." My argument is that constrained code is easier to inspect, check, replay, compile, and explain.

A workflow that actually closes

For me, the philosophy only becomes interesting when it turns into an actual loop.

The workflow I have in mind looks like this: give Claude or Codex a prompt for a module that fetches JSON over HTTP and prints a summary.

The first draft may look fine, but if it calls Http.get without declaring ! [Http.get], Aver rejects it at type-check time. If the pure parsing helper has no clear examples, that is an obvious gap for verify. If the flow is effectful, the repo's record/replay support gives you a deterministic way to exercise it.

That leads to a workflow like this:

aver check file.av
aver verify file.av
aver compile file.av -o out/

For pure logic, the center of gravity is verify.

For effectful code, it is record/replay:

aver run file.av --record recordings/
aver replay recordings/ --test --diff

That split is one of Aver's better ideas. Pure behavior is specified locally with examples. Effectful behavior is captured once against the real world, then replayed deterministically offline as a regression suite.

aver context is not part of execution. It is part of inspection. It is less a build step than a discovery tool: an agent can inspect a module with a fixed budget, for example aver context file.av --budget 10kb, get the contract-level map first, and only then decide what deserves deeper reading. That is a better fit for AI-assisted code exploration than forcing every model to ingest raw source from the start.

The interesting part for me is not that Aver helps AI generate code.

It is that Aver narrows what counts as acceptable generated code.

Why aver compile -> Rust matters

This is one of the most practical parts of the project for me.

aver compile turns an Aver module graph into a normal Rust/Cargo project. That gives me the split I wanted from the start:

• use Aver as the generation and review surface
• use Rust as the deployment surface

That matters because it answers the obvious objection: "Nice philosophy, but how does this ship?"

It also makes some of Aver's restrictions look less ideological and more pragmatic. No closures means simpler variable resolution and fewer translation headaches. Immutable data and pattern matching map cleanly. Explicit effects make the source easier to reason about before you ever compile it.

There is also a proof export path for the pure subset. That is interesting. But Rust is the killer feature here because it makes the workflow operational, not just conceptual.

The actual bet

I would not sell Aver as a universal replacement for general-purpose languages.

It is repetitive on purpose. Many developers will hate the lack of loops, closures, and other familiar shortcuts. It is also fair to look at some examples and think "this still resembles a very strict small FP language."

But I do think Aver asks a more serious question than most AI programming discourse:

If AI writes the first draft, should language design still optimize mostly for keystrokes?

Or should it optimize for auditability?

I made Aver pick auditability and push that choice into the grammar.

That is what makes it interesting to me. It treats hidden behavior as the real liability in AI-written code. Not as a tolerable side effect of convenience, but as a thing to design against.

If generated code becomes normal, that tradeoff may stop looking extreme and start looking necessary.

Repo: github.com/jasisz/aver

Manifesto: jasisz.github.io/aver-language