DEV Community: Szymon Teżewski

I Added Parallelism to a Language Without Adding async/await

Szymon Teżewski — Thu, 02 Apr 2026 21:34:06 +0000

Most languages that grow a concurrency story eventually grow a second vocabulary: async, await, tasks, futures, channels, executors.

That stack can be powerful, but it also leaks into everything. It changes APIs, changes mental models, and tends to spread once it arrives.

I wanted to try something narrower.

What if the language already had the shape I needed?

The idea

Aver already has tuples.

A tuple is a product of values:

(a, b)

So I added one operator:

(a, b)!

That means:

"These computations are independent. The runtime may evaluate them sequentially or in parallel."

And then one more:

(a, b)?!

That means:

"These computations are independent Result computations. If they all succeed, unwrap them. If one fails, propagate an error."

That is the whole user-facing feature.

No futures.
No task handles.
No scheduler API.
No user-visible thread model.

Just products and independence.

Why this fits Aver

Aver is intentionally explicit and structurally simple.

It already leans on:

immutable data
pattern matching
recursion instead of loops
explicit effects

So ! and ?! fit the language surprisingly well.

For pure code, independence is almost boring:

(fib(30), fib(31))!

For effectful code, independence is a declaration by the author:

(fetchProfile(userId), loadSettings(userId))?!

That means the semantics stay small:

the language says the branches are independent
the runtime chooses an execution strategy
the result stays deterministic

The nice part: recursion composes naturally

Once you have independent products, recursive fan-out becomes natural.

fn fetchStep(url: String, rest: List<String>) -> Result<List<String>, String>
    ! [Http.get]
    data = (fetchOne(url), fetchAll(rest))?!
    match data
        (body, others) -> Result.Ok(List.prepend(body, others))

That gives you recursive fork/join without inventing another abstraction.

And for bounded concurrency, I added List.take and List.drop, so windowing stays simple:

fn processInWindows(urls: List<String>, windowSize: Int) -> Result<Unit, String>
    ! [Http.get, Console.print]
    match urls
        [] -> Result.Ok(Unit)
        _ ->
            bodies = fetchAllParallel(List.take(urls, windowSize))?!
            processAll(bodies)?
            processInWindows(List.drop(urls, windowSize), windowSize)

That is still "just products plus recursion".

The same idea gives you pipeline parallelism:

fn pipelineContinue(ready: String, remaining: List<String>) -> Result<Unit, String>
    ? "Processes one ready item while fetching the next."
    ! [Http.get, Console.print]
    match remaining
        [] -> process(ready)
        [url, ..rest] ->
            data = (process(ready), fetchOne(url))?!
            match data
                (_, nextBody) -> pipelineContinue(nextBody, rest)

Item N is being processed while item N+1 is fetched. One independent product inside a recursive step, and you get production and consumption overlapping.

The hard part was not syntax

The syntax was tiny.

The hard part was defining a narrow semantic envelope and then making every backend actually respect it.

The first boundary was soundness. For pure terms, ! is sound by construction: tuple elements have no data dependency on each other, and Aver does not give them mutation or shared state to fight over. For effectful terms, ! is not proven. It is an unchecked contract from the author: "all schedules the runtime is allowed to choose are acceptable here." That turns out to be enough for the cases I wanted, without pretending I solved effect commutativity in general.

The second boundary was replay. If branches may reorder, replay cannot match by position. A branch that was "second" in one run might be "first" in another. So replay records grouped effects under a key shaped like:

(group_id, branch_path, effect_occurrence, effect_type, effect_args)

branch_path is the branch identity inside nested products. "0.1" means: outer branch 0, then inner branch 1. effect_occurrence disambiguates repeated effects inside the same branch. Without it, "the second Http.get in branch 0.1" collapses into "some Http.get in branch 0.1", which is not enough to replay nested or recursive programs deterministically.

The third boundary was cancellation priority. cancel is an execution artifact, not the primary failure. So when ?! unwraps results, a real Result.Err always beats a sibling cancellation error. That sounds like a small detail, but it is exactly the kind of rule that decides whether a feature feels principled or improvised.

I also had to be honest about cancellation

cancel sounds great until you ask what it actually means.

In Rust, there is no safe "kill this thread now" button. And honestly, that is good.

So Aver's cancel mode is cooperative.

In aver.toml:

[independence]
mode = "complete"
# mode = "cancel"

complete: all branches run to completion, then the leftmost real error wins
cancel: once one branch fails, siblings are signaled to stop at checkpoints

That is an important distinction.

Reducing wasted work, not promising rollback of the universe.

Backend reality

One of the most satisfying parts of this work was getting beyond "the docs say this should work" and forcing the backends to prove it.

Today the picture is:

interpreter: sequential, but semantically valid
VM: parallel independent products with cooperative cancel
compiled Rust: parallel independent products with cooperative cancel

I also added an end-to-end compiled regression test that compiles an Aver program to Rust, builds the generated Cargo project, runs it in both modes, and verifies that sibling work is shortened only in cancel. That test found real bugs, which is exactly why I wanted it.

Safety checks matter more than syntax sugar

The language lets authors declare effectful independence.

That is powerful, but it is also easy to misuse.

So aver check now emits independence-hazard warnings for likely bad branch pairs.

Today it warns for things like:

Console.* with Console.*
Console.* with Terminal.*
Tcp.* with Tcp.*
HttpServer.* with HttpServer.*
mutating Disk.*
mutating Http.*
mutating Env.*

And it shows up as a reviewable warning:

warning[independence-hazard]: Independent product branches 1 and 2 use potentially conflicting effects [Console.print, Terminal.flush] (shared terminal/output hazard)

"You can do this, but do not lie to yourself about the risks."

That turned out to be exactly the right tone for the feature.

What I like about this design

The best part is not that Aver now has parallelism.

The best part is that it got a concurrency story without becoming "an async language".

The feature stayed:

small in syntax
explicit in semantics
compositional with recursion
honest about effects

And that feels rare.

Too many language features start small and then explode into a second language inside the language.

Independent products still feel like they belong to the same design.

What is still intentionally missing

I did not add:

channels
streams
backpressure
task handles
futures as a surface concept
a general-purpose scheduler model

That is deliberate.

If this feature ever becomes a hidden path toward rebuilding worse async/await, I will have missed the point.

Its strength is that it is narrow.

The bigger takeaway

This project reminded me of something I keep relearning:

good concurrency features are often not about exposing more machinery.

They are about exposing the right semantic claim.

In Aver, that claim is:

"These computations are independent."

Once that is explicit, a lot of useful behavior can emerge from one small operator.

And if your runtime, replay model, diagnostics, and tests are strong enough, that one operator can carry a lot more weight than it first appears to.

If you want to look deeper

The core docs live here:

If I write a follow-up, it will probably be about the unglamorous part that mattered most:

how replay semantics, cancellation, and backend parity ended up being more important than the surface syntax.

Aver: Your codebase has no API for AI

Szymon Teżewski — Tue, 31 Mar 2026 10:21:11 +0000

A few projects have started calling themselves "AI-native" or "AI-first" languages. The pitch is usually the same: fewer tokens, one way to write things, simpler syntax. The metric is input cost — how cheaply can an LLM produce a file.

The bottleneck is not generation cost. It's comprehension cost: can the next agent that touches this code understand what it does, what it's allowed to do, and why it was written this way — without reading every line? Generation is fast and getting cheaper. Understanding is slow and getting more expensive, because the information an agent needs is almost never in the source text itself.

Aver is an AI-native language built around this problem. Not "fewer tokens in." More understanding out.

Every codebase is an archaeology site

Give Claude or GPT a Python project and ask it to add a feature. It reads files — lots of files. It guesses which ones matter. It infers intent from variable names and comments that may be outdated. It has no reliable way to know which functions talk to the network, which ones are pure, and which architectural choices were made deliberately vs. inherited from a Stack Overflow answer in 2019.

The AI is reconstructing information that the original author had but didn't encode in the artifact. Intent, constraints, design rationale — all of it exists only as implicit patterns in the code, if it exists at all.

The code has no API for the thing that reads it most often.

Token efficiency is real. It's just not the whole problem.

There's a popular thesis in the AI-first language space: fewer options, fewer libraries, a shorter spec for the model to memorize. Reduce choice paralysis, reduce token cost, and the language becomes better for AI.

That's a real optimization target. A language that takes 900 tokens to produce a CRUD endpoint instead of 1,800 is genuinely cheaper to generate. But a short program is not a legible program. You can win on token efficiency and still end up with code where the next agent doesn't know the intent behind a function, can't tell which calls have side effects, doesn't know why one approach was chosen over another, has no expected behavior to compare against, and has to regex-parse error output to figure out what went wrong.

Token efficiency helps code get written. A semantic surface helps code get understood, reviewed, repaired, and evolved. The Aver language doesn't compete primarily on fewest tokens to produce a program. It competes on most preserved meaning after the program exists.

What an AI-first language exposes to agents

The language encodes intent, effects, architectural decisions, and expected behavior as part of its grammar — parsed, type-checked, enforced, and exportable:

fn fetchUser(id: String) -> Result<HttpResponse, String>
    ? "Fetches a user record by ID from the external API."
    ! [Http.get]
    Http.get("https://api.example.com/users/{id}")

The ? line is a description literal — part of the function's signature, parsed by the compiler, exported by tooling. It's not a comment next to code; it's a declaration about the code that the toolchain knows about.

! [Http.get] is a declared effect — enforced statically and at runtime. If the function body calls Disk.writeText without declaring it, that's a compile error. An agent reading this signature knows the complete set of side effects without reading the body.

These ideas aren't novel individually. What matters is that they compose into a single exportable surface — and that there's a concrete command that exports it.

`aver context`: where an agent enters the codebase

This is the central piece.

When an AI agent starts working on an Aver project, it doesn't read source files. It runs aver context. This is the intended interface — the front door to the codebase for any agent.

aver context examples/core/calculator.av

Output:

## Module: Calculator

> Safe calculator demonstrating Result types, match expressions,
> and co-located verification. Errors are values, not exceptions.

### `safeDivide(a: Int, b: Int) -> Result<Int, String>`
> Safe integer division. Returns Err when divisor is zero.
verify: `safeDivide(7, 0) => Result.Err("Division by zero")`,
        `safeDivide(0, 5) => Result.Ok(0)`,
        `safeDivide(9, 3) => Result.Ok(3)`

### `safeRoot(n: Int) -> Result<Int, String>`
> Returns Err for negative input, Ok otherwise. Uses match on a bool expression.
verify: `safeRoot(0 - 1) => Result.Err("Cannot take root of negative number")`,
        `safeRoot(0 - 99) => Result.Err("Cannot take root of negative number")`,
        `safeRoot(0) => Result.Ok(0)`

### Decision: NoExceptions (2024-01-15)
**Chosen:** "Result" — **Rejected:** "Exceptions", "Nullable"
> Exceptions make error paths invisible at the call site.
> Result forces the caller to acknowledge failure explicitly,
> which is essential when AI tooling reads cod…
impacts: `safeDivide`, `safeRoot`

No implementation details. Signatures, descriptions, effects, expected behavior from verify blocks, and the design decisions that constrain the module. In ~2k tokens the agent gets the contracts before the implementation. Compare that with dumping 50k tokens of raw source into a context window.

aver context app.av --budget 10kb
aver context app.av --focus processOrder
aver context app.av --decisions-only

Start high, zoom in. The agent reads the contract map first, then drills into the functions that actually need attention.

Failures are parseable, not just readable

When something breaks, aver check emits structured diagnostics with repair suggestions and source snippets:

error[type-error]: Function 'wrongReturn': body returns String but declared return type is Int
  at: test_errors.av:30:1
     |
  30 | fn wrongReturn() -> Int
     |                     ^^^  declared Int
  31 |     ? "Returns wrong type (type checker error)."
  32 |     "oops"
     |     ^^^^^^  returns String

warning[perf-string-concat]: string concatenation with `acc` in recursive call
  at: lint_demo.av:20:31
  in-fn: repeat
  repair: O(n²) per iteration; consider collecting into a list and joining

Every diagnostic has a machine-readable slug, a source location down to the column, and a repair suggestion. --json emits the same as NDJSON — same schema across check, verify, and replay — so an agent can categorize errors and apply fixes programmatically.

Decisions survive across sessions

The hardest information to preserve across AI sessions is why. An agent can re-derive what the code does by reading it. It cannot re-derive why it was written that way.

Aver's decision blocks encode rationale as first-class syntax:

decision TailRecurrenceForPerformance
    date = "2026-02-24"
    reason =
        "Naive fib(n-1)+fib(n-2) is exponential and easy for AI to generate."
        "Tail recursion makes fib linear time and predictable."
    chosen = "TailRecursion"
    rejected = ["NaiveRecursion"]
    impacts = [fib, fibTR]

Parsed, validated, exported via aver context --decisions-only. When an agent touches fib three months from now, it reads this block and knows the exponential version was considered and rejected — with an explicit reason.

I haven't seen many languages treat architectural rationale as grammar rather than convention. That doesn't mean it's a solved problem — enforcing decision quality is still on the author. But the toolchain exposes rationale the same way it exposes types and effects.

Record/replay closes the loop on effects

Pure functions have verify blocks. Effectful code has recordings. aver run --record captures every effectful interaction with caller, arguments, and outcome. aver replay --test --diff re-executes against that recording deterministically. If the code drifts, you get a structured diagnostic — which effect changed, in which function, at which step.

What this adds up to

Aver composes intent, effects, decisions, expected behavior, and structured failures into one exportable surface. aver context is the entry point. The rest of the toolchain feeds into it. The agent gets contracts before implementation, rationale before refactoring, and parseable failures when things break.

Aver is early and incomplete. But this semantic surface already works today. The repo is here, the manifesto is here. cargo install aver-lang, point aver context at a module, and read what comes out.

Previous posts: A prompt is a request, a language is the law | The most boring games you have Aver seen | I gave my language VM four memory lanes

I Gave My Language VM Four Memory Lanes Instead of a Normal Heap

Szymon Teżewski — Fri, 20 Mar 2026 14:14:34 +0000

Most language runtimes eventually converge on the same story: allocate objects into a heap, add a garbage collector, spend the next few years arguing about generations, barriers, and pause times.

For Aver, that story started to feel wrong.

Aver is a small language designed for AI-assisted development. It is intentionally narrow — immutable data, match as the only branching construct, recursion and tail calls instead of loops, no closures, explicit effects, and a lot of very small helper functions.

That shape matters. Once I added a real bytecode VM, it became obvious that a generic "heap + GC everywhere" design would leave a lot of performance and clarity on the table. The control flow of the language was already telling me something about lifetime.

So instead of treating all heap-backed values the same, the VM now uses four memory lanes: young for local scratch work, yard for tail-call survivors, handoff for ordinary return survivors, and stable for real escapes.

This post is about why that model emerged and why I think it is one of the most Aver-shaped parts of the runtime.

The premise

One of the traps in runtime work is assuming that the natural unit of memory management is "a function call".

In Aver, it is not.

Aver programs have a lot of small functions. A helper might exist just to wrap a value in Result.Ok, reshape a record, do one small match, or delegate to another helper. If the VM pays full boundary-management cost on every one of those, you spend too much time being correct about memory and not enough time doing work.

So I pushed the runtime toward a more semantic model. Temporary scratch data dies aggressively. Loop-carried state survives tail-call reuse. Helper return values survive into the caller — but do not pretend to be globally long-lived. Only real escapes become truly stable.

Four lanes.

The four lanes

One thing first: the lanes hold heap-backed values only. Small ints, bools, floats, and many VM-known function references stay inline as NaN-boxed 8-byte handles and never touch the arena. A lot of the traffic in Aver programs is scalar, and scalar traffic avoids arena churn entirely.

`young` — scratch

The default lane. Most temporary work starts here — string building, temporary records and tuples, list intermediates, wrapper cells. At a frame boundary, the VM knows exactly what part of young belongs to the current frame. It truncates that suffix in one shot.

The important thing about young is what it doesn't do. It does not pretend that temporary work might be long-lived. It does not hedge. When the frame is done, everything that was not explicitly moved somewhere else is gone.

`yard` — tail state

If a frame is being reused by TAIL_CALL_*, loop-carried values need to survive the reset.

fn countdown(n, acc)
    match n
        0 -> acc
        _ -> countdown(n - 1, List.prepend(n, acc))

Here n is an inline int — never touches the arena. But acc is a growing List, heap-backed. It is not "global". Not even "ordinary return state". It is data that must survive the next tail-call iteration and nothing more. Each time through, scratch work lands in young and dies in bulk. acc persists in yard until the recursion bottoms out.

`handoff` — return lane

Suppose a helper returns a Record to its caller. That value should not stay in the callee's young — the callee's scratch memory is about to die. But it also should not go straight into some globally long-lived space.

Return survivors get their own lane.

handoff is not always a copy destination. If the compiler sees a value in an obvious return position, it may build it directly in handoff. Otherwise it starts in young and gets evacuated at return time. Either way, the return path ends in handoff.

`stable` — real escape

Values go here only when they truly escape — globals, host-facing values, top-level-completed results. Any source lane can feed stable: a value in young, yard, or handoff that crosses an escape boundary gets compacted into stable by an explicit root-driven walk.

stable is not a generational GC old-gen. It is not "the place where everything eventually goes because the runtime got scared". It is a canonical space for values that have genuinely outlived the current call-chain story.

That distinction is what keeps the model clean.

What actually happens

Here is what a helper return looks like at runtime. The syntax is pseudo-Aver (the real thing would look a bit different), but the shape is right:

fn build_label(name, count)
    let prefix = String.concat("item-", name)
    let label = Record { tag = prefix, n = count }
    label

fn main()
    let result = build_label("alpha", 42)
    ...

"alpha" and 42 are inline — they sit in the value stack as NaN-boxed handles, no arena allocation. String.concat produces a new Str in young, local scratch work. The Record is heap-backed — if it is in an obvious return position, it may get built directly in handoff. Otherwise it starts in young and gets evacuated on return.

When build_label returns: the Str from concat is in young, nothing in handoff or yard points to it, young gets truncated, the Str is gone. The Record in handoff survives into main.

No GC pass. No mark phase. No full generational barrier machinery. Scratch dies in bulk, the return value was already in the right lane, and there is coarse global dirty tracking for the cases that need it.

Why not just use a GC

GC is not bad. But for this language shape, a lot of memory death is obvious from control flow.

When values die because a frame is done, or because a tail-call iteration resets scratch state, a full general-purpose collector is overkill. What the VM does instead is closer to region-style allocation for local scratch, relocation of the live graph when something must survive, and explicit canonicalization only at real escape boundaries.

Runtime cost ends up tied to live survivors, not to total historical allocation volume.

That is what I wanted.

Tiny helpers were still too expensive

At one point the VM was technically correct, but real workloads still felt slower than they should have.

Not the four lanes. Granularity.

If every function behaves like a full-blown memory boundary, you pay too much bookkeeping for helpers that exist mostly for readability. That led to two extra ideas.

Thin functions. If a function returns without growing young, yard, or handoff, and without dirtying globals, the VM skips the boundary relocation path entirely. A few comparisons, pop frame, continue.

Parent-thin functions. The more Aver-specific trick. Some wrapper-like helpers borrow the caller's young lane directly. Normal call frame, but no separate scratch lifetime. If they stay out of yard and handoff, their temporary work lives in the caller's scratch space and dies with the caller.

A very weird optimization in generic VM terms. Also exactly the kind of thing that becomes available when the language is small and constrained enough.

Benchmarks

This is not just a story anymore. In recent local benchmark runs, the VM is consistently faster than the tree-walking interpreter on real workloads — often by a lot.

Benchmark	Interpreter	VM	Speedup
`sum_tco(1M)`	`1998.911ms`	`668.600ms`	`3.0x`
`countdown(1M)`	`1434.012ms`	`563.250ms`	`2.5x`
`result_chain(40K)`	`330.243ms`	`83.964ms`	`3.9x`
`shapes(30K)`	`378.891ms`	`71.828ms`	`5.3x`
`list_builtins(40K)`	`135.254ms`	`53.888ms`	`2.5x`
`mixed_real(20K)`	`233.029ms`	`58.676ms`	`4.0x`

The memory side matters just as much. In many of those runs, the VM finishes with live+ = 0 in places where the interpreter still keeps large amounts of data alive. Scratch memory is getting reclaimed at the right boundaries.

End-to-end app benchmarks: workflow_engine seed_tasks dropped from 44s to 33s, list_tasks from 544ms to 332ms. payment_ops show_payment barely moved — 14ms to 13ms — but it was already fast.

The story is not "VM beats everything always". The story is: once there is enough real work, the VM starts paying back its representation and lifetime model.

The honest trade-off

The model is good. It is not free.

The implementation gets subtle fast. Four lanes, thin fast paths, parent-thin fast paths, direct allocation into non-default lanes — that is not "a simple arena" anymore. That is a real memory system. I had to clean up a large amount of duplicated traversal and relocation code recently, because that kind of duplication becomes dangerous fast in a runtime like this.

My honest take: the architecture is right, the implementation must stay aggressively maintained. The model earns its complexity — but only because the benchmarks and real workloads actually moved.

Why I like this

The best runtime ideas feel inevitable in retrospect.

Aver is immutable, recursion-heavy, explicit, small enough that semantics still matter more than compatibility baggage. So instead of copying a generic memory story from a mainstream VM, the runtime can follow the language.

Not "I implemented a fancy allocator". More:

the memory model reflects the control-flow model of the language

young, yard, handoff, stable are not just implementation tricks. They are the runtime version of a language design decision.

That is the kind of systems work I want more of.

Aver is open source: github.com/jasisz/aver

If you want the lower-level design note, the repo includes a technical VM document covering the bytecode model, list representation, and memory lanes in detail.

The most boring games you have Aver seen

Szymon Teżewski — Wed, 18 Mar 2026 08:42:17 +0000

Yesterday Claude built Snake and Tetris in Aver. I did not write the implementations. I reviewed the decisions.

That distinction is the whole point.

No if/else. No loops. No mutable state. No exceptions. Game loops through tail-recursive calls. Every side effect declared in the function signature. The games work. You can play them. But playability is not the point. The review loop is.

What "boring" means here

Here is the Snake game loop:

fn gameLoop(state: GameState) -> Result<String, String>
    ? "Render, sleep, read input, tick — TCO recursive"
    ! [
        Random.int,
        Terminal.clear, Terminal.flush, Terminal.moveTo, Terminal.print,
        Terminal.readKey, Terminal.resetColor, Terminal.setColor,
        Time.sleep,
    ]
    render(state)
    Time.sleep(state.tickMs)
    tick(readInput(state))

No surprises. You can see the intent (?). You can see every effect the function is allowed to perform (!). You can see the data flow: render, sleep, read input, tick. State goes in, state comes out. If this function tried to make an HTTP call, the type checker would reject it.

Here is collision detection:

fn checkCollision(state: GameState) -> Bool
    ? "True if the snake hit a wall or itself"
    match List.get(state.snake, 0)
        Option.Some(head) -> match checkWall(head, state.width, state.height)
            true -> true
            false -> bodyContains(state.snake, head, 1)
        Option.None -> true

verify checkCollision
    checkCollision(gs([pt(5, 5)], 1, 0, pt(0, 0))) => false
    checkCollision(gs([pt(0, 5)], 1, 0, pt(0, 0))) => true
    checkCollision(gs([pt(5, 5), pt(6, 5), pt(5, 5)], 1, 0, pt(0, 0))) => true

No if. Every branch is a match. The verify block sits right next to the code it tests. You do not need to open a second file. You read the function, you read the examples, you move on.

This is boring. That is the point.

Three layers of review

Claude wrote both games. But "I reviewed them" understates what actually happened. There are three layers, and I am only the last one.

Layer 1: The compiler. Claude's first attempts had wrong syntax — match with colons, records with braces, || instead of Bool.or. The parser rejected them. Claude fixed them. I never saw these errors.

Layer 2: aver check. Missing verify blocks, undeclared effects, uncovered match arms — the static checker caught structural problems that compiled but violated Aver's contracts. Again, Claude fixed them without my input.

Layer 3: Me. By the time I looked at the code, it was syntactically correct, structurally complete, and passing all verify blocks. I was not debugging. I was making design calls.

Claude's first Tetris draft used List<List<Int>> for the board. It worked. It even dutifully recorded this choice in a decision block. But in review I immediately saw the problem: an Int tells you nothing. Is 1 a T-piece or an L-piece? I said "make a PieceKind sum type" — and Claude rebuilt it, replacing the old decision with a new one explaining why the sum type is better.

That is the beauty of the loop: the AI documents every design choice, even the bad ones. The reviewer's job is not to find bugs — it is to upgrade the decisions.

Then I told it to split the single file into modules — separate the piece definitions from the board logic from the rendering. Tetris ended up as four modules (board, pieces, logic, main), each under 250 lines. Claude did it, adjusted the imports, kept the verify blocks passing.

The toolchain catches mechanical errors. The checker catches structural gaps. The human makes architectural calls: better types, better structure, better boundaries. The kind of feedback that takes thirty seconds to give and would take thirty minutes to implement by hand.

And then the proofs check themselves

aver proof exports the pure subset of an Aver module to Lean 4 or Dafny. Verify cases become proof obligations — confirmed by the Lean kernel or Z3, not by a test runner.

What passes today, out-of-the-box, zero manual fixes: 72 example-level proofs across Snake and Tetris (collision detection, grid operations, piece rotations, movement). Plus 3 universal theorems on Tetris scoring:

theorem computeScore_law_tetrisDoublesSingle :
    ∀ (level : Int), computeScore 4 level = 8 * computeScore 1 level

That is not "for these inputs." That is "for every level in the game." Lean unfolds the definition, omega closes the arithmetic. Formal proof, zero axioms, zero sorry.

Not everything is covered yet. Functions using index-based recursion lack termination proofs, which currently blocks some Tetris cases. The limitation is in the code generator, not the language.

Even with those gaps, the same source file that Claude wrote and I reviewed also generates formal proofs that neither of us wrote by hand. Three outputs from one source: interpreter for iteration, Rust for deployment, Lean or Dafny for proof.

Design by inconvenience

Aver is inconvenient for humans to write and convenient for humans to review. That tradeoff used to look irrational. In an AI-first workflow, it starts to look obvious.

AI does not care about constraints. The model generates the verbose version in milliseconds. The cost of verbosity falls on the author — and when the author is a language model, that cost is zero. The benefit falls on the reviewer — and when the reviewer is a human under time pressure, that benefit is everything.

Boring code, not boring programs

The games are playable. The Snake moves, eats food, grows, dies. The Tetris pieces rotate, drop, clear lines, keep score. The programs are not boring at all.

The code is aggressively boring. And that is the whole thesis: boring is a property of the source, not the output. You want the source boring so you can review it. You want the output to do whatever it needs to do.

There are sibling efforts approaching this from the other direction. Prove makes code hard for AI to generate correctly — the compiler rejects until intent is demonstrated. Aver makes code easy for AI to generate but boring enough for humans to review. Same diagnosis, different treatment.

In a world where AI writes the first draft, review time is the bottleneck. Boring code compresses review time. That is the rational response.

Aver is open source and experimental: github.com/jasisz/aver

Snake source: examples/games/snake.av
Tetris source: examples/games/tetris/

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

Szymon Teżewski — Thu, 12 Mar 2026 09:18:17 +0000

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

DEV Community: Szymon Teżewski

I Added Parallelism to a Language Without Adding async/await

The idea

Why this fits Aver

The nice part: recursion composes naturally

The hard part was not syntax

I also had to be honest about cancellation

Backend reality

Safety checks matter more than syntax sugar

What I like about this design

What is still intentionally missing

The bigger takeaway

If you want to look deeper

Aver: Your codebase has no API for AI

Every codebase is an archaeology site

Token efficiency is real. It's just not the whole problem.

What an AI-first language exposes to agents

aver context: where an agent enters the codebase

Failures are parseable, not just readable

Decisions survive across sessions

Record/replay closes the loop on effects

What this adds up to

I Gave My Language VM Four Memory Lanes Instead of a Normal Heap

The premise

The four lanes

young — scratch

yard — tail state

handoff — return lane

stable — real escape

What actually happens

Why not just use a GC

Tiny helpers were still too expensive

Benchmarks

The honest trade-off

Why I like this

The most boring games you have Aver seen

What "boring" means here

Three layers of review

And then the proofs check themselves

Design by inconvenience

Boring code, not boring programs

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

Make intent part of the program

Design by inconvenience

A workflow that actually closes

Why aver compile -> Rust matters

The actual bet

`aver context`: where an agent enters the codebase

`young` — scratch

`yard` — tail state

`handoff` — return lane

`stable` — real escape

Why `aver compile -> Rust` matters