Reference
Tooling
Because every structural fact is on the source surface, the compiler already computes what an IDE or a model needs to query. A long-lived daemon serves it. There is no separate doc generator, annotation scraper, or linter re-deriving what the typechecker already knows.
The compiler as a service
The CLI is one client of the compiler, not the compiler itself. The IDE is a second client over LSP, and a model is a third over MCP. All three talk to one daemon that holds the parsed AST, the elaborated MIR, the type environment, the obligation and spec caches, and the structure index in memory, keyed by content hash. The core is synchronous on purpose, so a given project state and query always return the same answer.
MCP
The Model Context Protocol is how a model talks to the compiler: the same typed protocol the IDE uses. Seven namespaces are fixed for V1.0, and method shapes do not change across V1.x, so a client written once keeps working.
| Namespace | Handles |
|---|---|
client.* | handshake, project and document lifecycle |
build.* | check, build, run, test, bench |
codegen.* | spec materialization |
inspect.* | AST, diagnostics, structure map, contract diff, completions, synthesis |
edit.* | structural edits, addressed by qualified name |
typecheck.* | trust points, decreases obligations, traces |
layout.* | comptime size, align, offset |
Adding a precondition and verifying it is two calls, edit.signature.requires.add then build.check, both answered from the same in-memory state with no file written in between.
The structure map
For each directory of source, the compiler writes an index.toon from its own data structures. It stays in sync because there is no separate annotation to drift. Each entry carries the full signature, the functions it calls, the transitive effects it can reach, the refinements on it, the specs it instantiates, and every trust point: a list of each place the verifier was told to take a claim on faith.
Reading stays directory-sized
The map only helps if a directory's index stays small, so the compiler warns when one would exceed a line threshold, or when filenames encode a hierarchy that should be a directory. The defaults pull a codebase toward depth-first layout from the first file.
Structural edits
An edit is a function of the source, the edit spec, and a target named by qualified name rather than line, so it survives changes around it. Edits apply as one in-memory transaction. Renaming a field rewrites every use or rolls back whole. Generated spec artifacts are read-only.
Diagnostics and synthesis
A diagnostic is a structured object: its class, the span in bytes and line-column, the elaborated form the typechecker saw, the chain of in-scope facts, a counterexample written as concrete edda values, and suggested edits in the shape an LSP code action expects. The compiler can also propose code, either as typed completions ranked by how well they satisfy the refinements in scope, or as goal-directed synthesis that searches for a body discharging the ensures clause against the same solver the build uses.
The command line
Each verb maps one-to-one to an MCP method.
| Command | Does |
|---|---|
edda check | typecheck and discharge refinements, no codegen |
edda build | check, then codegen and link |
edda run | build and execute |
edda test --properties | run tests, including properties derived from refinements |
edda structmap --check | emit the structure map, or fail if it is stale |
edda contract-diff a b | report the contract change between two refs |
edda lint --trust-points | list every trust annotation in scope |