If AI is going to write more of the first draft, what should the source look like for the human reviewer?

Aver is an experimental statically typed language and toolchain for AI-written, human-reviewed code.

My bet is that source code should carry more than implementation. In most projects, implementation survives in the code, but intent lives in docs, decisions live in ADRs or tickets, and expected behavior lives in tests that may or may not stay close to what they describe.

Aver tries to make those parts first-class: explicit method-level effects in function signatures; ? strings for machine-readable function intent; decision blocks for design choices and tradeoffs; colocated verify blocks for pure functions; deterministic record/replay for effectful flows; aver context for compact contract-level module export; aver compile to Rust; and aver proof to Lean 4 for mechanical proof checking of the pure subset.

A small pure example:

  fn charge(account: String, amount: Int) -> Result<String, String>
      ? "Pure charge validation and transaction-id creation."
      match amount
          0 -> Result.Err("Cannot charge zero")
          _ -> Result.Ok("txn-{account}-{amount}")

  verify charge
      charge("alice", 100) => Result.Ok("txn-alice-100")
      charge("bob", 0)     => Result.Err("Cannot charge zero")

An effectful wrapper looks like this:

  fn chargeAndPrint(account: String, amount: Int) -> Result<Unit, String>
      ? "Effectful wrapper around charge."
        "Prints the transaction id on success."
      ! [Console.print]
      result = charge(account, amount)
      match result
          Result.Ok(txn) ->
              Console.print(txn)
              Result.Ok(Unit)
          Result.Err(err) ->
              Result.Err(err)

Aver is intentionally opinionated: no exceptions, no null, no `if`/`else`, no loops, no closures. Branching goes through `match`, failure through `Result`, absence through `Option`, and side effects are explicit.

The repo includes small examples, but also `projects/workflow_engine`, which is my attempt at a medium-sized auditable application core with app/domain/infra split, replayable effectful flows, and verify-driven pure logic.

This is still early. I’m not claiming everyone should replace mainstream languages with Aver.

The narrower question I’m testing is whether making intent, decisions, checks, and effect boundaries machine-readable inside the source makes AI-produced code easier to review, constrain, and trust.

I’d especially like feedback on whether this feels like a language worth existing, or whether the same idea should just be conventions and tooling on top of an existing language.