This started as the first external Aver user requesting missing functionality. n1bor wanted to try Aver and write a Bitcoin node listener in it. It struck me as both: the niche for Aver I was only sometimes shyly dreaming about, and something I have no clue about.

Do I have to tell you this found a lot of holes in the language itself? Every bigger pre-existing project in Aver was written by one of my agents, and they all shared similar instructions, so you may imagine it was not the ideal field test. The Bitcoin listener was really valuable because it not only exposed new ways of using actual Aver, but unveiled a lot of my blindspots about built-in effects and the whole ecosystem.

I won’t pretend that Aver, even after almost half a year of work, is… ready to use. It is far from it, which is funny as hell and a bit depressing. But then the first real user comes in and uncovers something deeper about existing effects. I knew this was coming, I was even slightly preparing for that, but you can never be prepared for the real world.

What effects are in Aver

Aver had effects from the very beginning, and the word covers more than it usually does. An effect is anything a function does to the outside world or needs from it — what the literature splits into effects and coeffects. Console.print changes something. Time.now changes nothing, it just demands something. One annotation, both directions, because I didn’t want two questions where there is one.

Underneath it is finer than that. Args.get is a snapshot, Random.int is generative, Console.print is output, Disk.writeText is both — and that classification, not the word, is what replay and proofs actually run on. On the surface it is one small list: Args, Console, Disk, Env, Http, Random, Tcp, Terminal, Time.

Each of them has to have an implementation in each of Aver’s backends. It has to state how it is treated in proofs and how hostile verification approaches it, listing the corner cases. So you can imagine that adding one is not a simple task right now.

And then the first requests land: Tcp byte methods and SHA-256. Ok, let’s add those. Tcp is a no-brainer, it is a pre-existing effect with gaps. SHA-256 is a bit more interesting, because it is a pure computational method. It means it cannot be an effect, because it can even potentially be written in pure Aver (only if Aver had bit operators at the time), it can be neatly implemented for proofs as a real function, and so on. The distinction falls out quite clean.

Then comes Postgres

The next request, from the same person, is Postgres. On the surface it is no different: Postgres is a missing piece and there is no good way to use it in Aver right now. You either agree that Postgres somehow becomes a built-in effect, or you implement Postgres on raw binary sockets in Aver. Both are painful and tedious, but doable.

Why Aver has no packages

Aver does not have a notion of a package at all. All code in Aver is local, and dependencies are only referenced locally from your own disk. I was even half-joking that if Aver ever needs a package manager I am calling it Morphine.

It is not that I hate dependencies. But if I have to be honest about Aver’s whole premise — that writing code becomes cheaper, but we should value trust and clear boundaries — I have to reject the notion of packages and package managers. This is the only logical thing to do if you really believe in it. Why should you trust a whole dependency, which may be chained to other dependencies, if they are not coming from you at all? Isn’t it better to tell your agent “I need this and that”, so the agent basically creates a custom version of it for you?

Postgres is a particularly good example, because I can even think about it not having to have ORM-like abstractions at all. Each table you query may just return the specific type you asked about, isn’t that neat? Or you may abstract the whole of Postgres as one possible kind of purely hypothetical Store that can be swapped for something else later. Both ways are simply more interesting than going through a forced abstraction of SQL or an ORM.

Capabilities and providers

So I have to stop thinking about effects as built-in, carved-in-stone compiler magic. And I have to stop thinking about all of this as effects touching the outside world, because half of it doesn’t touch anything. The next requests made that obvious: cryptographic functions, public-key infrastructure, JSON parsing, LevelDB. They all make sense and they all sit somewhere else on the scale. LevelDB is Postgres again. Crypto functions are SHA-256 again, except I’m much less keen on writing elliptic-curve cryptography in Aver, unless somebody really wants it… slow but provable.

Capabilities (+ providers) are what I want to build right now.

A capability doesn’t have to be an effect. It is a contract: my program needs this thing, and something has to provide it on the target I want to run on. Some of them are effectful because they touch the outside world — Store, File, Random. Some are not effectful at all. RIPEMD-160 is a function. Checking an elliptic curve signature is a function. Why should either of them make every caller effectful, just because the fast implementation happens to come from a Rust library?

Aver implements neither kind. A provider does, and for a Store that provider can be LevelDB, Postgres, or a directory full of files. For a pure crypto capability it can be some well-tested native library. The program never sees any of that, it sees the contract it asked for. Providers differ per target — VM, compiled Rust, wasm, proofs — and a target without one just can’t run your program.

Here is what one looks like today:

module Store
    kind = capability
    intent = "A key-value store the program requires and a provider supplies."
    exposes []
    effects []

opaque Handle

operation open(path: String) -> Result<Handle, String>
    ? "Open a store at a location the provider understands."
    oracle = generative
    replay = recorded
    hostile = [openOk, openDenied]

operation get(handle: Handle, key: Bytes) -> Result<Option<Bytes>, String>
    ? "Read one value. A missing key is Option.None, not an error."
    oracle = generative
    replay = recorded
    hostile = [getFound, getMissing]

operation put(handle: Handle, key: Bytes, value: Bytes) -> Result<Unit, String>
    ? "Write one value."
    oracle = generativeOutput
    replay = recorded
    hostile = [putOk, putRejected]
    unmodelled = [compaction]

An operation has no body, because a capability never says how anything gets done. Handle is opaque on purpose — its layout is the provider’s business, and writing it down here would chain every future provider to whatever the first one happened to do.

The attributes are the part I like most. oracle and replay say what happens when the operation gets lifted into a proof, and what happens when its effects are recorded and replayed. hostile names the stubs that hostile verification is allowed to throw at every caller. And unmodelled is where you admit out loud what the contract doesn’t cover. Compaction happens, nobody above the boundary can see it, and now at least the contract says so.

Portability has to stay visible

This can’t turn into an invisible escape hatch, and there is a very concrete reason. Tcp is portable because somebody standardised it first — on wasip2 it lowers onto wasi:sockets/tcp. There is no wasi:postgres, and there never will be. WASI 0.2 doesn’t have TLS either. So a Store with only a native provider falls outside the proof boundary and outside portability at the same time. Right now you find that out at --target wasm-gc, which is far too late to be any use.

What I want is to be able to ask, before anything runs:

Store.get
  VM        provided
  Rust      provided
  wasm-gc   missing
  wasip2    host import
  Lean      oracle
  Dafny     model

The last two lines matter more than they look. How something runs and how something is proven are two different questions. A capability can have a real model in Lean, or an oracle interpretation, or a pile of attached assumptions, or no proof support at all — and none of that follows from whether it runs through Rust, a host import or a browser.

Which is why this has to keep six things apart, not one: the contract, effect semantics, replay semantics, proof interpretation, runtime provider, target availability. Call it all “FFI” and you have collapsed six decisions into a single word.

Where the package ends

And yes, a provider can use a package. Which sounds like I rejected packages and then reinvented them with extra steps. The difference is where the package ends.

An Aver program doesn’t import the whole LevelDB API and doesn’t let LevelDB types crawl through its code. It imports its own Store contract. LevelDB sits behind one small boundary and claims to implement exactly those operations. Swap it for Postgres and nothing above the boundary changes. If the contract was designed well, of course. That is a big if.

This doesn’t make the provider trustworthy. If a crypto library is wrong, your result is wrong, and no Aver contract is going to repair a corrupted LevelDB using the power of types and positive thinking. What you get is smaller: the assumption is one thing, in one place, and you can see it. The rest of the program doesn’t have to swallow the whole dependency just to use it.

Maybe reuse was a price, not a virtue

I think this is one of the bigger changes coming from AI writing code. Reuse mattered so much because writing software was expensive. If writing another parser, another adapter, another Store implementation for your exact domain is cheap, then importing a generic abstraction with twenty years of accumulated options stops being the obvious move.

This doesn’t mean agents should reimplement databases or cryptography. Please don’t let an agent casually invent your elliptic curve because I wrote a paragraph against package managers. Some software is hard because the problem is hard, not because humans type slowly. That stuff still makes sense as an external provider. What disappears is the pile of reusable code sitting between your application and those hard boundaries.

JSON is a nice example. Aver already has a JSON parser written in pure Aver. It is readable, provable and currently quadratic. For a config file, fine. For 100MB, not fine. You should be able to keep the local one, ask an agent to make it faster, or bind a fast parser as a pure capability and say out loud that you trust it to behave. Three different choices, and I don’t want the language quietly making one of them for you.

So maybe future programs have more local code, fewer dependencies, and more explicit capabilities. The boring logic gets generated for this application and no other. The hard machinery stays outside, behind small contracts. Effects, replay, proof assumptions and target availability hang off those contracts instead of being scattered through compiler tables or buried three levels deep in somebody’s dependency tree.

That is what I mean by code getting cheaper while trust gets expensive. Generated code isn’t trustworthy just because it sits on your disk. But you can read it, check it, verify it, and throw it away together with the program. You can’t inspect a provider the same way, so the least Aver can do is tell you exactly where the assumption starts.

None of this exists yet

None of this exists yet in usable form. Aver parses the first capability declarations and then flatly refuses to compile them, because accepting a contract while enforcing nothing would be worse than not having it at all:

$ aver check store.av
Check: store.av
error[capability-unsupported]: capability declarations are parsed but not yet supported: module 'Store' declares `kind = capability`, but nothing acts on it yet, so the module is checked exactly like an ordinary one. Remove the line until capability support lands.
  at: store.av:2:1
  repair: Remove the capability declaration. The grammar is accepted so the shape can be reviewed, but no operation is registered and no boundary is enforced yet.
    |
  2 |     kind = capability
    | ^

Every declaration gets its own refusal, not just the first one the scan trips over. check, verify and proof all refuse the same way, including when the capability sits one module away in a dependency. The grammar landed before the semantics, and the gap between the two is exactly where a false guarantee would move in.

I am still figuring out the exact model, and some of it is going to turn out wrong.

But this time I have something better than another example written by one of my agents. I have a real program waiting for LevelDB, binary files and cryptography. If the capability design is bad, the Bitcoin listener will find out before I do.

Now the hard part is telling my very first user: you are not getting LevelDB any time soon, but you are getting a fishing rod. I am fairly sure that is not what the issue asked for.