A language I'm building to make AI-written code safer.

01 — WHY

I can't read everything my agents write anymore.

AI agents write a lot of my code now. I think that is going to be true for a lot of people soon, and review does not scale to it.

So I wanted a language where more of the safety comes from the compiler and less from somebody reading carefully. Something I can lean on for code I didn't write.

I think Rust is the language you'd want AI to write. But honestly I'm not a strong Rust programmer, and I never got used to ownership. Almide is my attempt to keep that kind of safety without making anyone, person or agent, write the ownership part.

It is statically typed, compiles to native code through Rust, and emits WebAssembly directly. It has Option and Result, exhaustive pattern matching, and explicit effect declarations.

02 — NOTHING TO GET WRONG

You don't write ownership. The compiler infers it.

type Order = { id: Int, items: List[String], total: Int }

fn large(orders: List[Order]) -> List[Order] =
  orders |> list.filter((o) => o.total > 500)

fn main() -> Unit = {
  let orders: List[Order] = [
    { id: 1, items: ["pen", "ink"], total: 260 },
    { id: 2, items: ["desk"], total: 900 },
  ]
  let big = large(orders)
  println("${list.len(orders)} orders, ${list.len(big)} large")
  for o in orders {
    println("${o.id}: ${list.join(o.items, ", ")}")
  }
}

$ almide run orders.almd --target wasm
2 orders, 1 large
1: pen, ink
2: desk

orders is passed to large and then used again in the loop. Nothing in the source says moved, borrowed or copied. No lifetimes, no free.

The compiler works out where every heap value is created, shared and consumed, with a Perceus-style inference. The two targets then carry that out differently. Native output is Rust, and Rust's own drops do the freeing. Wasm uses reference counting.

03 — THE PART I CARE ABOUT

The compiler doesn't get to grade its own work.

I don't trust my own compiler. I built it with AI agents, so why would I?

Every time it builds Wasm, the compiler has to write down evidence of what it did: every place it shares or frees a value, every array index it checked. A separate program reads that evidence. If it doesn't add up, there is no output file.

A rejection is not your bug. It is the compiler's, and the build says so:

error[certificate-rejected]: app.almd: almide-verify judged this build's
certificate and did not accept it (exit 1)
  app.wasm was not written: the build's own certificate does not hold,
  which is a compiler bug — please report it

Abridged. The verifier's own report follows the first line.

04 — TRUST SPINE

The checker can have bugs too. So there are four.

One checker would just move the trust somewhere else. These four are built in different ways, so the same mistake is unlikely to be in all of them. Together with the evidence they check, the project calls this the Trust Spine.

In CI, Proofcore, Proofcast and Buildgate have to reach the same verdict on every piece of evidence, for every program in the test corpus. A rejection from this setup has already caught a real miscompile in my compiler.

The proofs are 46 Rocq files in the repository, 654 theorems and lemmas in about 21,700 lines. They are about the checker and its models, not about the compiler.

What the evidence is about

The evidence comes in kinds, one per property. Each kind has its own rule, and the rule is what the four checkers apply.

These hold for the code the evidence covers. Byteanchor re-checks the bounds, init and fields events against the bytes, and matches the recorded reference-count events against the calls in the file. Events it cannot tie to an instruction are counted as unlocated, not passed silently.

05 — WHEN THE CODE IS WRONG

The error tells the agent what to change.

Agents make mistakes. What matters is what happens next. An agent that learned other languages will write items.length:

error[E013]: no field 'length' on list
  --> app.almd:3:14
  in field access .length
  here: println("${items.length}")
  hint: Almide values have no fields — use the `list` stdlib module.
  try: (machine-applicable — `almide fix` applies it)
      list.len(items)

$ almide fix app.almd
  Applied 1 machine-applicable fix-it(s) from diagnostics: E013 at line 3

That one is mechanical, so the tool applies it. A misspelled function name is different:

error[E002]: undefined function 'string.lenn'
  hint: Did you mean `string.len`?

$ almide fix app.almd
1 diagnostic(s) have `try:` snippets that need manual application:
  [E002] app.almd:3:14  undefined function 'string.lenn' (maybe-incorrect)

Compiler output from 0.69.0, abridged.

That is a guess about what the author meant, so it stays a suggestion. I'm trying to keep the line between a mechanical repair and a decision about intent visible in the tooling.

06 — MISTAKES THAT DON'T SHIP

A forgotten case is a compile error. So is an ignored failure.

The edit mistake I see most from agents: add a variant to a type, and miss one of the places that has to handle it.

type Shape =
  | Circle(Float)
  | Rect(Float, Float)
  | Triangle(Float, Float)      // added

fn area(s: Shape) -> Float = match s {
  Circle(r) => 3.14159 * r * r,
  Rect(w, h) => w * h,
}                               // not updated

error[E010]: non-exhaustive match: missing Triangle(_, _)
  --> shape.almd:6:36
  hint: add arms for Triangle(_, _):
  Triangle(arg1, arg2) => _

Failure works the same way. A call that can fail gives you a Result, and you have to say what happens to it. Dropping it on the floor is an error, not a warning.

effect fn load(path: String) -> String = {
  let text = fs.read_text(path)     // can fail, and nothing says so
  text
}

error[E041]: implicit propagation of this binding's value was removed —
this value is a Result
  --> load.almd:4:14
  hint: Write `expr!` to propagate, or consume the Result as a value
  (`??`, `?`, match ok/err).

Compiler output from 0.69.0, abridged.

One character fixes it: fs.read_text(path)!. The point is that the author had to decide, and the decision is visible in the source.

07 — ONE SOURCE, TWO TARGETS

Native and WebAssembly from the same source, held to the same output.

Native builds go through Rust. WebAssembly is emitted directly by the compiler, with no LLVM in between. Hello world comes out as a 325-byte .wasm file.

Two backends can disagree. So every observable promise is written down as a contract, 454 of them today, each tied to executable evidence. CI runs 1,055 programs on both targets and compares stdout, stderr and the exit code. A third executor, an interpreter that runs the program before any code is generated, votes as well.

The comparison holds under documented conditions. Randomness, clocks and platform details have their own scoped contracts, and the interpreter abstains on 17 programs it can't run.

08 — WHAT ELSE IS IN IT

It is a whole language, not a demo.

09 — WHAT IS NOT DONE

It is not finished, and I want to be clear about that.

• The compiler as a whole is not proven. The proofs cover the checker and its models.
• Native builds don't run the verifier. They go through a certified renderer, and the whole test corpus now does. But the evidence is judged in the project's verification, not at your build, and a program the renderer can't handle still falls back to the standard code generator.
• On your machine only one of the four checkers runs. The other three run in CI, on the test corpus. If the verifier isn't installed, a Wasm build goes through unchecked.
• Some evidence is partial. A certificate that covers only part of a program is let through. Component output is not checked this way.
• Not every recorded event is tied to an instruction yet. Byteanchor reports the ones it cannot locate as unlocated. That number is not zero everywhere.
• A program can pass every check and still compute the wrong thing. None of this is about whether the logic is right.
• I can't show that agents write Almide better than Rust or TypeScript. My first measurement was about 100% in every language with a strong model, so it told me nothing.
• It is pre-1.0. There are known bugs and things will change.

The full account of what is proven and what is only trusted is in the repository: proven vs trusted.

10 — HOW IT WAS BUILT

I built this with AI agents. That is the point.

The compiler is written in Rust, and I used AI agents heavily to write it. I'm saying that up front because some people will not want to look at a project built that way, and that is fair.

But it is also why the project looks the way it does. If agents write the compiler, I can't vouch for it by having read it. So it has to produce evidence, and something else has to check the evidence. That is the same problem everyone using agents is about to have with their own code. Almide is me working on it in the open.

11 — TRY IT

See where it breaks.

The playground runs in your browser with nothing to install. To install the compiler and the verifier on macOS or Linux:

curl --proto '=https' --tlsv1.2 -fsSL \
  https://raw.githubusercontent.com/almide/almide/main/tools/install.sh | sh

The installer needs the GitHub CLI (gh) to verify the release attestation. Windows and source builds are in the README.