The design of edda

Everything on the signature

function load(rfs: ReadOnlyFilesystem, path: String, allocator: Allocator) -> String
    with {rfs, allocator, err: fs.FsError}
    requires path.len() > 0
    ensures  result.len() > 0

One line of signature answers four questions. The effect row with {rfs, allocator, err: fs.FsError} lists what the function can do; the row is closed, so what is not listed cannot happen. The parameter modes state ownership at the call site: let borrows, mutable borrows for writing, take consumes, init fills in. There are no lifetime annotations; the modes carry the information lifetimes would, with nothing to propagate across files. The requires and ensures clauses constrain the values that may enter and leave.

Reading the signature is a complete account of the function's behavior toward the rest of the program. Nothing else in the language is allowed to add to it.

Authority is a parameter

The rfs above is a capability: a value that carries the right to read the filesystem. Capabilities cannot be created — Filesystem.new() is rejected. They arrive as parameters to main and flow down from there, narrowing one-way as they go: a filesystem scoped to one directory, a network bound to localhost, an allocator capped at a byte budget. There is no ambient filesystem, clock, or network anywhere in the language.

The security consequence falls out by construction. A dependency cannot phone home unless its caller hands it a network. A child process receives a subset of what its parent holds, never more. Auditing what a program can reach means reading the parameters of its entry point.

Contracts the build proves

The requires and ensures clauses are not documentation. The compiler turns them into obligations and an SMT solver discharges them on every build; no binary exists until the proofs hold. The built-in obligations come for free: integer overflow, slice indexing, division by zero, and narrowing casts each carry a proof requirement at the site.

Verification is a dial, not a switch. Most functions carry no refinements and cost the build nothing beyond typechecking. Proof concentrates where a wrong value would do damage — a buffer index, a capability boundary, a state machine that must not skip a step. Each mechanism bounds a different kind of behavior:

Where a proof is out of reach

The solver is decidable, not omniscient. Two annotations cover the gap. @unverified skips discharge for one function; the compiler still synthesizes property tests from its refinements, so the waived contract is exercised rather than assumed. @trust accepts one obligation at one site. Both require a written reason, and both are listed by edda lint --trust-points.

There is no assume keyword. An axiom could quietly manufacture a false certificate; a trust point cannot. The trust-points list is the complete set of places the verifier was told to take a claim on faith, so the safety posture of a program is a fact it states about itself, auditable in full.

Nothing resolves out of view

For the signature to be the whole truth, nothing may rewrite or re-route the code behind it. So there are no generics, no traits, no macros, no operator overloading, no runtime reflection, and no inheritance. Reuse goes through spec: a template the compiler expands into named, concrete, content-addressed modules. Runtime polymorphism is sum types with exhaustive matching. Errors are values in the err: T effect, propagated by ? — a function's failure modes are part of its row, not discovered at runtime. Optional values are sum types; there is no null.

One form per construct, and the source matches the runtime: if it runs, grep finds it. What stays from C++ and Rust is not negotiable — total memory control, zero-cost abstraction, no required runtime, first-class FFI, deterministic destruction.

No comments

The lexer rejects every comment token. A comment can only restate what the code says or claim what no local check can validate, and once stale it reads as fact while being fiction. Every job a comment used to do has a checked home instead: claims about behavior live in effect rows and contracts the solver discharges; descriptions are derived into the structure map from checked facts; rationale lives in the tracker. The only free text left in source is the mandatory reason on an explicit trust annotation.

The consequence: every token in an edda source file is either executable or compiler-verified. There is no third category of plausible prose, and no way for a description to drift from what it describes.

The structure map

Because every fact about a function is on its signature and nothing in source can go stale, the compiler can write the documentation itself. Every build emits an index.toon per directory from type-checker data: each signature, its effect row, its refinements, what it calls, and every site where verification was waived. The map is never written by hand and never out of date.

A reader takes in a directory from its map, then opens only the source files the change actually touches. The input needed to reason about a directory is bounded by the directory, not by the codebase around it.

Here is a real one — the map beside std/lib/collections/sort/src, trimmed to the i64 family. Every field is read from the type checker, never written by hand: the signature, the pure effect row (empty), what each function calls, and the contracts it carries.

loc: src

functions[4]{name,file,line,end,visibility,stability,sig,eff,cone,calls}:
  sort.sort_i64,sort.ea,5,8,public,,"(slice: mutable [i64]) -> ()",,=,quicksort_i64 | slice.len
  sort.quicksort_i64,sort.ea,10,21,module,,"(slice: mutable [i64], lo: usize, hi: usize) -> ()",,=,partition_i64 | quicksort_i64
  sort.partition_i64,sort.ea,23,67,module,,"(slice: mutable [i64], lo: usize, hi: usize) -> usize",,=,slice.len
  sort.is_sorted_i64,sort.ea,69,81,public,,"(slice: [i64]) -> bool",,=,slice.len

invariants[4]{target,file,line,rule}:
  sort.quicksort_i64,sort.ea,11,decreases (hi - lo)
  sort.partition_i64,sort.ea,24,requires (lo < hi)
  sort.partition_i64,sort.ea,25,ensures (result >= lo)
  sort.partition_i64,sort.ea,26,ensures (result <= hi)

Architecture is a build error

A bounded read only stays bounded if directories stay small. So the bound is enforced: every directory's interface has a token ceiling, and one that grows past it fails the build with the split computed from the call graph. Here is what that failure looks like:

error[structure_map_too_dense]: Gate A (per-node, red):
  lib/scrapy/src index.toon is ~10635 tokens — 4635 over
  the 6000-token ceiling — splits into 8 call-disjoint groups:
  {main, route, serve}, {extract}, {frontier}, {model},
  {robots}, {scheduler}, {search}, {taxonomy}
  note: fan into 8 sibling subdirectories one level down

Gate A caps what any one directory costs to read; Gate B keeps parent directories thin, so descending the tree stays cheap at every level. file_low_cohesion flags files that fuse unrelated call clusters, and filename_encodes_hierarchy pushes structure into the directory tree where the map carries it. In most ecosystems a degraded architecture is a review comment; here it is a failed build, with the seam to fix it named in the error.

Why the pieces are inseparable

Each decision is a precondition for the next. Concrete codegen is what lets grep find every use of a name, which is what makes a mechanical rename safe. Authority on the row is what makes contract-diff exact, which is what makes an automated edit to a critical function reviewable. The absence of comments is what keeps the structure map trustworthy, which is what makes the bounded read possible, which is what the token gates protect. Generics would break grep; ambient authority would break contract diff; macros would break structural edits. Remove one piece and the rest stop holding.

The result is a codebase where reading any part costs a fixed amount, every claim encountered while reading has been machine-checked, and a wrong edit fails to compile with a counterexample. Iteration gets faster as the program grows, because the input never does.

The name comes from Snorri Sturluson's 13th-century Edda, a single written record meant to carry a complete body of knowledge forward. The language puts that record in the compiler.