experimental · pre-1.0 · windows x86-64
Designed for a future of programming.
Edda bets that most code will soon be written by machines, and is designed for that author: every function carries contracts the compiler proves on every build, and every build emits a map of the whole project that an agent reads instead of guessing. The bet is open — no model has edda in its training data yet, and until one does, the compiler does the heavy lifting.
Working with an AI agent? The machine-readable setup recipe is /get-started/agent.txt.
function advance(cursor: i64, len: i64) -> i64
requires cursor < len
ensures result <= len
{
return cursor + 2
}error[refinement_unproven]: ensures clause 0: (result <= len)
note: counter-example:
note: len = 1
note: result = 2
note: cursor = 0The guard checks for one step; the body takes two. Instead of shipping that, the build hands back the exact input that breaks the claim. Change the requires to cursor + 2 <= len and the proof goes through. Most languages would have shipped it.
Your agent reads the map
Every edda build writes an index.toon file into each source directory: the type checker's own record of every signature, effect, contract, and call edge in it. No human writes it, so it can never drift from the code. Here is the real one sitting beside the standard library's sorter:
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)Edda's own compiler is 197,000 lines of source across 770 directories; the maps for all of it total 20,000 lines, a tenth the size. Your agent reads the map for the directory it is changing, then opens only the spans it needs. A doc generator summarizes comments; this is the type checker publishing what it proved. The design page shows how the maps stay truthful; the tooling page covers the compiler daemon your agent queries directly.
What the compiler guarantees
Each of these is checked on every build. The compiler enforces them, so nobody has to remember.
Provably wrong code does not build
Contracts, integer overflow, array bounds, and division by zero are all proven by a solver during the build. A failed proof names the exact input that breaks the claim.
The docs are compiler output
The map above is regenerated from checked facts on every build. Edda has no comments at all: what you read is what the type checker proved, as current as the code itself.
Refactors land whole or not at all
The compiler runs as a daemon holding the checked project in memory; your editor talks to it over LSP, your agent over MCP. A rename targets a qualified name and rewrites every use, or touches nothing.
Every function declares what it can see and touch
To read a file, a function must be handed the filesystem. To dial out, a dependency must be passed a Network capability by your code. The signature is the audit.
No task outlives its scope
Every task handle ends in exactly one of await, cancel, or detach, and a scope waits for all of its children before it returns. Fire-and-forget does not compile.
Status: experimental
We are bootstrapping a language with itself. The compiler is written in edda, and it type-checks its own 197,000-line source through its own backend; a Rust bootstrap compiler builds it today and defines the reference behaviour while the self-hosted compiler matures.
Windows (x86-64) is the platform we build and test on today; Linux and macOS releases are rolling out through CI. The site you are reading is rendered by a verified edda program.
Today's models find edda genuinely hard to write. Habits imported from Rust or TypeScript produce code that does not parse. In our own testing, an agent building the same program spends consistently more tokens in edda than in TypeScript, and the compiler rejects much of what it first writes. The rejections are the design doing its job: each one is a mistake that would have shipped silently elsewhere. Still, if you expect the fluency your agent has in a mainstream language, edda does not have it yet.
The compiler, the 24,000-line standard library, the 28,000-line package ecosystem, and the 165,000-line Rust bootstrap were all written by LLM agents working against the compiler's own checks. There was no edda to train on. When the self-hosted compiler retires the bootstrap, the entire toolchain becomes edda, proven by edda.
Build it in edda
Web services & APIs
Ship handlers that list every failure they can raise, on a server that takes its socket as a capability through main. Its entire reach is written in one signature.
Command-line tools
Build one static binary with no runtime to install. The entry signature lists every file, socket, and process the tool can ever reach.
Embedded & firmware
Target bare metal with no garbage collector and no hidden allocations. Memory bounds live in the signature, proven at build time, with layout exact to the wire.
WebAssembly & the edge
Compile to a sandbox that already agrees with the language: a module's imports are the parameters of its main function, so the host grants exactly what the code declares.
Get involved
Read the design — how the language is built up, one decision at a time.
Contribute — the compiler, standard library, and this site are developed in the open.
Join r/EddaLang — questions, showcases, and release threads; or write to ea@edda-lang.org.