[{"_1":2,"_3":-5,"_4":-5},"loaderData",{"_5":6,"_7":8,"_9":10},"actionData","errors","root",{"_122":123},"routes/modules.$creator.$moduleId",{"_14":15,"_16":17,"_18":19,"_20":21},"routes/modules.$creator.$moduleId.endpoints",{"_11":12,"_13":-5},"error","Module not found","tools","module",{"_20":22,"_23":24,"_25":26,"_27":28,"_29":30,"_31":32,"_33":34,"_35":26,"_36":37,"_38":-5,"_39":-5,"_40":-5,"_41":42,"_43":44,"_45":46,"_47":48,"_49":50,"_51":52,"_53":54,"_55":-5,"_56":48,"_57":58,"_59":60,"_61":-5,"_62":-5,"_63":-5,"_64":-5,"_65":66,"_67":68,"_69":70,"_71":72,"_73":74,"_75":-5,"_76":-5,"_77":-5,"_78":48,"_79":-5,"_80":81,"_82":83,"_84":85,"_86":87,"_88":89,"_90":91,"_92":93},"apiUrl","https://odel.app/api","creator","deed-lang","moduleId","deed","@deed-lang/deed","displayName","Deed","tagline","Contract-first language and MCP server for capability-aware code and patch review.","iconKey","https://avatars.githubusercontent.com/u/309664262?v=4","category","local","status","published","visibility","public","metaDescription","deploymentType","external","workerName","bindingName","mcpConfig","pricingModel","free","creatorUserId","system:external-import","createdAt",1786773650000,"updatedAt",1788778772000,"sourceRegistry","official-mcp-registry","sourceUrl","https://registry.modelcontextprotocol.io/v0/servers?search=io.github.deed-lang%2Fdeed","sourceVerified",true,"sourceMissingSince","importedAt","upstreamStars",8,"upstreamUpdatedAt",1786748709000,"detectedTransport","detectedAuthType","probeStatus","lastProbedAt","githubRepoUrl","https://github.com/deed-lang/deed","githubRepoFullName","deed-lang/deed","releaseId","ext-deed-lang-deed","version","0.2.13","descriptionMarkdown","

\n \n \n $\"Deed\"$ \n \n

\n\nA contract-first language where a function signature is a promise the compiler checks.\nBuilt for code that machines write and humans review.\n\n> **Status: the toolchain works; adoption is the open question.** The compiler lexes,\n> parses, resolves names, checks types, contracts and effect rows, and runs programs through\n> either the reference interpreter or a WebAssembly backend. `deed build` writes a core\n> module, and `--component` writes a component when its exported values cross the canonical\n> ABI. Programs get authority from explicit capabilities, with the same host rules in both\n> engines. The largest unfinished technical work is value reclamation and wider component\n> adapters; the largest project risk is simpler and measured: no public repository outside\n> this organization contains known Deed source yet. [ROADMAP.md](https://github.com/deed-lang/deed/blob/main/ROADMAP.md) keeps that\n> distinction and the commands that measure it.\n\n## Getting it\n\nOne line, on Linux or an Apple-silicon Mac:\n\n```\n$ curl -fsSL https://raw.githubusercontent.com/deed-lang/deed/main/install.sh | sh\n```\n\nOn Windows:\n\n```\n> irm https://raw.githubusercontent.com/deed-lang/deed/main/install.ps1 | iex\n```\n\nEither one downloads the release asset for your machine, refuses it if its hash\nis not the one the release published, and puts a single file in your own profile.\nIt never asks for a password, because it never writes outside it. The checksums\ncome from the same release as the binary, so that catches a corrupted download\nand does not catch a compromised release; saying so is better than a `sha256`\nthat reads like it proves more than it does.\n\nBy hand instead: every release carries a `deed` binary for Linux, macOS and Windows.\nTake the one for your machine from\n[releases](https://github.com/deed-lang/deed/releases), unpack it, and run it.\nThere is nothing else to install: the compiler, the formatter, the test runner and the\nlanguage server are all in that one file.\n\nStart with the [tutorial](https://github.com/deed-lang/deed/blob/main/TUTORIAL.md) if you want one program built up one step at a time.\n\n```\n$ tar xzf deed-v0.2.13-x86_64-unknown-linux-gnu.tar.gz\n$ ./deed-v0.2.13-x86_64-unknown-linux-gnu/deed --version\ndeed 0.2.13\n```\n\nWith Rust 1.88 or newer instead, from crates.io or from a clone:\n\n```\n$ cargo install deed-lang\n$ cargo install --path crates/deed-cli\n```\n\n`deed` on crates.io belongs to somebody else, so the package is `deed-lang`.\nThe binary it installs is `deed`; the [package README](https://github.com/deed-lang/deed/blob/main/crates/deed-cli/README.md)\nkeeps the short install and MCP entry points next to the package metadata.\n\n**What the version promises.** `0.x` says the language can still move, so a file that\ncompiles against one minor release may not compile against the next. Breaking moves are\ncalled out in release notes, and `deed fix` carries the mechanical part when possible. The\nfull policy, including diagnostics and `std/`, is in\n[design/07-versioning.md](https://github.com/deed-lang/deed/blob/main/design/07-versioning.md).\n\n## Starting something\n\n`deed new` writes a project rather than leaving you to work out the module header\nand the file layout from this repository. The name becomes both the directory and\nthe module path.\n\n```\n$ deed new greeter\ngreeter/greeter.deed\ngreeter/main.deed\n\nnext: cd greeter && deed test .\n\n$ cd greeter\n$ deed test .\n./greeter.deed\n ok a greeting carries the name it was given\n ok there is no greeting for nobody\n ok property greeting (100 cases)\n\n3 passed, 0 failed\n\n$ deed run main.deed\nhello, world\n```\n\nThree tests from two files, and only two of them were written down. The third is\ngenerated from the contract on `greeting`, which is what a signature being a\npromise buys. There is no manifest, because a manifest here says where code\noutside your tree lives and a new project has none.\n\n`crates/deed-cli/tests/new.rs` runs that command into a temporary directory on\nevery commit and then checks, tests, runs and format-checks what came out, so the\nscaffold cannot rot into something that no longer compiles.\n\n## What it looks like on real code\n\n```\n$ deed run examples/config.deed --dir examples\nfound it\n`..` would leave the directory, and there is no way out of a `Dir`\n`../Cargo.toml` is not a single name, and a `Dir` only takes one at a time\n`/etc/passwd` is not a single name, and a `Dir` only takes one at a time\n`nowhere` is not there\nused the fallback\n```\n\n```\n$ deed test examples/\nexamples/counter.deed\n ok bumping twice adds twice\n ...\nexamples/transfer.deed\n ok moves the money and conserves the total\n ok refuses to overdraw and leaves the ledger alone\n ok refuses a currency mismatch and leaves the ledger alone\n\n138 passed, 0 failed\n```\n\nThat number used to be 102. Seven of those tests are in `std/table` now, because the table\nlibrary stopped living under `examples/` and a module that ships with the compiler is context\nrather than subject, so the corpus does not run its tests any more. Nothing was deleted: the\nmodules that ship carry one hundred and ten tests of their own, and\n`crates/deed-driver/tests/shipped.rs` runs every one of them on every commit.\n\n```\n$ deed check examples/transfer.deed --obligations\nobligations: 7 proven, 0 tested, 6 guarded\n guarded examples/transfer.deed:94:5 transfer ensures ok\n ...\n proven examples/transfer.deed:202:76 Positive\n```\n\nFor an editor, see [`editors`](https://github.com/deed-lang/deed/blob/main/editors). VS Code now carries both syntax\nhighlighting and a language-server client, while Helix and Neovim start the\nlanguage server from a few lines of configuration and no plugin.\n\nFor a coding agent, `deed mcp` speaks the Model Context Protocol on stdin and\nstdout, so the machine writing the code can ask the compiler the same questions\nan editor does rather than scraping them out of terminal output. It holds no\ncapability: a program arrives as text, the answer leaves as text, and a program\nwhose row reaches a file is refused before it runs.\nIts official Registry name is `mcp-name: io.github.deed-lang/deed`.\n[how-to/let-an-agent-use-the-compiler.md](https://github.com/deed-lang/deed/blob/main/how-to/let-an-agent-use-the-compiler.md)\nhas the tool reference and the one line worth reading.\n\n## Every agent patch comes with a receipt\n\n`deed review` compares the checked module set before a change with the one\nafter it. The first receipt names newly declared authority and obligations\nthat fell to a weaker contract tier:\n\n```\n$ deed review --before old/src --after src\nreceipt: review required\nauthority added (1)\n + billing/transfer/settle: Audit.note\nobligation tier regressions (1)\n ! billing/transfer/settle: Positive proven -> guarded\nguarded obligations added (0)\n```\n\nThe paths may name files or directories, and imports are resolved independently\non each side. `--format json` emits the same receipt as one stable object for an\nagent or CI job. Findings are informational unless a policy turns them into a\ngate: `--deny-new-authority`, `--deny-weaker-promises` and\n`--deny-new-guarded` each exit one when its own evidence is present, while still\nprinting the receipt and a policy verdict. A side that does not check is refused\nrather than compared.\n\nThe same evidence is available to an agent as `deed_review`. It takes the\nbefore and after module sets as arrays of source text, resolves imports within\neach array, and applies the same three policies without opening a file.\n[The CI guide](https://github.com/deed-lang/deed/blob/main/how-to/review-an-agent-patch-in-ci.md) is a complete pull-request\nworkflow that compares the two commit trees rather than a runner's mutable\nworking directory.\n\n## Demo\n\nOne clause in a function signature is the difference between two components.\n[demo/README.md](https://github.com/deed-lang/deed/blob/main/demo/README.md) shows two functions that are identical except\nfor one `uses` entry, compiles both to WebAssembly, and shows the import section\nof each module side by side. The test in\n`crates/deed-driver/tests/demo.rs` pins the host's refusal mechanically on\nevery commit.\n\n## How-to guides\n\nIf you already know the language and want the shortest path to a specific task,\nstart with [how-to/README.md](https://github.com/deed-lang/deed/blob/main/how-to/README.md). Those pages index the existing\ncorpus: checking a module set, writing tests, contracts and `assert refuses`,\neffects and capabilities, formatting, backend compilation, and editor setup.\n\nThe shipped library API is indexed separately in [docs/std.md](https://github.com/deed-lang/deed/blob/main/docs/std.md), with one\npage per module and every exported function held there by a documentation ratchet.\n`deed doc ...` writes the same page for any module of your own. There are no\nvisibility modifiers here, so every declaration is API and a page is the signature,\nthe row, the contract and the lines of its own tests that name it.\n\nThere is no REPL. A Deed input is a module of declarations, and `deed run` enters through\n`main` rather than evaluating a top-level expression. For quick experiments, use a scratch\n`.deed` file with `deed check`, `deed test` or `deed run`. The right browser answer is a\nplayground that edits and runs a whole program in that same shape.\n\nThere is also a small [conformance suite](https://github.com/deed-lang/deed/blob/main/conformance/README.md) for checks that should hold\nacross implementations.\n\nEvery `.deed` file here was written by one person, which is the largest open\nquestion about this language and not one the compiler can answer.\n[benchmarks/README.md](https://github.com/deed-lang/deed/blob/main/benchmarks/README.md) is where that stops being a sentence:\na set of tasks, each with tests it does not show the author, and a scorer that\nreports not only whether an answer compiles and passes but how much of its\ncontract the checker could prove.\n\nUser-visible language, diagnostics, library and tool changes are recorded in\n[CHANGELOG.md](https://github.com/deed-lang/deed/blob/main/CHANGELOG.md), including programs that used to compile and no longer do.\n\n## The idea\n\nMost of the code being written today is not typed out by a person. That changes which\ncosts matter. Producing a line of code is close to free. Reading it, trusting it, and\nfinding out three weeks later that it was subtly wrong are not.\n\nEvery language we use was shaped by the opposite assumption. They optimize for the\ncomfort of someone typing character by character: implicit behaviour, clever shorthand,\nfive ways to express the same thing. All of that is now working against us.\n\nDeed makes a different trade. Signatures carry the entire contract, bodies are checked\nagainst it, and nothing in the language lets a function reach outside what its signature\nadmits to.\n\n```deed\nfn transfer(from: AccountId, to: AccountId, amount: Amount)\n -> Result\n where\n from != to,\n uses\n Ledger.balance,\n Ledger.post,\n Audit.append,\n ensures\n ok => result.from == from,\n ok => result.amount == amount,\n ok => Ledger.balance(from).units == old(Ledger.balance(from).units) - amount.units,\n ok => Ledger.balance(to).units == old(Ledger.balance(to).units) + amount.units,\n ok => Ledger.total() == old(Ledger.total()),\n err => unchanged(Ledger),\n{\n ...\n}\n```\n\nThis is not an illustration. It is the top of [examples/transfer.deed](https://github.com/deed-lang/deed/blob/main/examples/transfer.deed),\nwhich the compiler lexes, parses, resolves, type checks and effect checks on every commit.\n\nThree things follow from that block, and they are the whole pitch:\n\n**You review the signature, not the body.** It fits on one screen and it is complete.\nWhoever wrote the body had nothing else to satisfy.\n\n**The body needs no other context.** No global state, no implicit conversions, no\ninheritance, no exceptions thrown from four frames down. Everything that can affect this\nfunction is written above the brace.\n\n**The function cannot reach the network.** Not by accident and not on purpose. It did not\nask for that capability in `uses`, so it does not have it, and it holds no value that would\nlet it name one. Sandboxing stops being a container and becomes a type.\n\n## Why this is a language and not a library\n\nA library can offer contracts. It cannot stop you from ignoring them, it cannot see the\nwhole call graph, and it cannot make the absence of an effect mean anything. Contracts,\neffects and capabilities are only useful if they are total, and total means the compiler\nenforces them.\n\nThe longer version, including the cost model this is all based on, is in\n[design/00-motivation.md](https://github.com/deed-lang/deed/blob/main/design/00-motivation.md).\n\n## Design documents\n\n| Document | What it covers |\n| --- | --- |\n| [00-motivation.md](https://github.com/deed-lang/deed/blob/main/design/00-motivation.md) | The cost model, and why a library cannot do this |\n| [01-principles.md](https://github.com/deed-lang/deed/blob/main/design/01-principles.md) | The constraints we are willing to be held to |\n| [02-syntax.md](https://github.com/deed-lang/deed/blob/main/design/02-syntax.md) | Contract blocks, types, errors, modules |\n| [03-effects.md](https://github.com/deed-lang/deed/blob/main/design/03-effects.md) | Effect declarations, propagation, handlers |\n| [04-capabilities.md](https://github.com/deed-lang/deed/blob/main/design/04-capabilities.md) | Authority, how it enters a program, and why |\n| [05-backend.md](https://github.com/deed-lang/deed/blob/main/design/05-backend.md) | Compiling to WebAssembly, and what does not change |\n| [06-grammar.md](https://github.com/deed-lang/deed/blob/main/design/06-grammar.md) | The grammar, checked against the parser both ways |\n| [07-checker-semantics.md](https://github.com/deed-lang/deed/blob/main/design/07-checker-semantics.md) | The checker rules the implementation enforces |\n| [07-editions.md](https://github.com/deed-lang/deed/blob/main/design/07-editions.md) | How a breaking change ships without splitting the ecosystem |\n| [characters.md](https://github.com/deed-lang/deed/blob/main/design/characters.md) | Why characters remain one-scalar strings |\n| [fractional-values.md](https://github.com/deed-lang/deed/blob/main/design/fractional-values.md) | The decision on fractional values and money |\n| [hash-map-requirements.md](https://github.com/deed-lang/deed/blob/main/design/hash-map-requirements.md) | What a hash map would require from the language |\n| [refusals.md](https://github.com/deed-lang/deed/blob/main/design/refusals.md) | Everything deliberately left out, and why |\n| [07-versioning.md](https://github.com/deed-lang/deed/blob/main/design/07-versioning.md) | Compatibility policy for language, diagnostics, and `std/` |\n\nRead them in order. Each one leans on the one before it.\n\n## What is built\n\n| Crate | Does |\n| --- | --- |\n| `deed-diagnostics` | Spans, source maps, and structured diagnostics with machine-applicable fixes |\n| `deed-lexer` | Source text to tokens |\n| `deed-ast` | The syntax tree |\n| `deed-parser` | Tokens to a tree, with recovery |\n| `deed-resolve` | Every name bound to a declaration, including across module boundaries |\n| `deed-typeck` | Every expression given a type, including types from other modules |\n| `deed-effects` | Every effect row checked against what the body does |\n| `deed-interp` | Runs `test` blocks, property tests and `main`, with contracts enforced |\n| `deed-fmt` | The one canonical form, with no options for the output |\n| `deed-lsp` | A language server: diagnostics, hover, go to definition, references, rename, completion, signature help, quick fixes, an outline, workspace search and formatting |\n| `deed-dap` | A debug adapter: breakpoints, stepping, the call stack and the bindings of every active call |\n| `deed-driver` | Runs all of the above, in one place, so nothing drifts |\n| `deed-lang` | The `deed` binary: `new`, `check`, `test`, `run`, `fmt`, `fix`, `lsp` and `debug`. Its directory is `crates/deed-cli` |\n\n`deed lsp` is a language server, and most of it is plumbing over things that already existed:\nthe compiler produces structured diagnostics with spans, `Types::type_of` can say what an\nexpression turned out to be, `Resolutions` can say where a name was declared, and the\nformatter has one canonical answer with no options. It publishes diagnostics as you type,\nsays the type of whatever is under the cursor, jumps to a declaration in whichever file\ndeclares it, lists every use of a name across the workspace, renames one everywhere it is\nwritten, offers what could be written where the cursor is, offers the patch a diagnostic is\nalready carrying, says what the file declares, and formats a file.\n\nSignature help is the one that is most this language's own. Everywhere else the contract is\non the screen already, because it is written on the declaration. At a call site it is not:\n`transfer(a, b, amount)` says nothing about what the call performs or what it needs to be\ntrue first, and that is exactly where somebody is deciding whether they can afford it. So the\nlabel carries the row as well as the types, and `shout(Console, String) uses Io.write -> ()`\nis the whole signature rather than the part that fits an editor's idea of one.\n\nIt is read off the text rather than the tree, for the same reason completion is. `add(` with\nnothing after it does not parse, and that is the moment the question gets asked. Nesting is a\nstack rather than a counter, so the comma in `add(add(1, 2), 3)` belongs to the inner call\nand the ones in `total([1, 2, 3], 4)` belong to the list.\n\nThat last one was data with nowhere to go. A diagnostic carries the edit that resolves it\nwhere the repair is unambiguous, and the only thing that could reach one was `deed fix` on a\ncommand line, which applies the certain ones and skips the guesses. So the guesses were\nreachable by nothing at all, and \"cannot find `lenght`, did you mean `length`\" knew the answer\nand made the reader type it. They are quick fixes now, and `Applicability` carries straight\nover: a machine-applicable fix is the one `deed fix` would apply without being asked, so it is\nthe preferred action, and a guess is offered and never preferred. The editor already had a\nword for the distinction and the compiler already had the distinction.\n\nCompletion is the only one that is a different shape. Everything else answers a question\nabout a name that already exists, and a document does not parse while somebody is typing into\nit, so it answers a narrower question instead: what is in scope here. After a `.` that is the\nfields of whatever is to the left; inside `use a/b.{ }` it is what that module exports, which\nis the one place a name has to match another file exactly; anywhere else it is what the file\ndeclared, what it imported, and the prelude. Nothing it offers inserts more than a name. No\nsnippets, no argument placeholders, no auto-import, because each of those is a decision about\nwhat somebody meant.\n\nThe outline is the one answer that does not go through a check. Everything else this server\nsays is about a name that resolved; an outline is about what is written, and half a\ndeclaration is still worth drawing while somebody is typing the rest of it, so it reads the\nparse tree of the one file and nothing else. What belongs to a declaration is nested under it,\nbecause a variant belongs to its choice and a handler operation belongs to its handler and a\nlist that said otherwise would be a worse version of scrolling. The protocol has fewer kinds\nthan this language has declarations, so a `type` and an `effect` share one: both are a named\nthing declared by its shape, and picking a different icon for one of them would be picking it\nfor how it looks rather than for what it is.\n\nRename and find references are the same walk with two answers, which is the point of them\nsharing one. A rename that edited the declaration and left the `use` line that brought the\nname into another file would fix one file and break another, and that is worse than not\nhaving rename at all. What it deliberately does not decide is whether the new name is a good\none: a collision with something already in scope is something the checker has a diagnostic\nfor, and answering it twice is how the two answers come to disagree. It does refuse a name\nthe language cannot hold, and it asks the lexer rather than holding a second definition of\nwhat an identifier is.\n\nIt checks a document together with every other `.deed` file in the folders the editor said it\nhas open, and an open file's text comes from the buffer rather than from disk, so removing an\nexport in one file puts a squiggle on the import in another before either is saved. The set\nof files is the workspace rather than a guess: `initialize` carries it, and taking what the\neditor says is the same answer `deed check src/` gives when a person says which directory they\nmean. An editor that names no folder gets the single file behaviour. That was the only\nbehaviour until recently, and it meant every file with a `use` in it had a red line under the\nimport, which is exactly the failure a server is not allowed to have.\n\nIt rechecks the whole workspace on every keystroke and on every hover. That used to be\nfollowed by \"and nothing has measured it\", which is now not true:\n`cargo run -p deed-driver --example edit_loop --release` says the recheck is linear at about\n82 microseconds per file, so 512 files cost about 42ms per keystroke, inside P9's 100ms\nbudget, and a few thousand files is where it leaves. It also says effectively all of that\nwork is spent on files that did not change, which is what a cache would take off. So the\ncache is worth writing when the size arrives and is not worth writing now, and that is a\nconclusion with a number behind it rather than a feeling. `design/01-principles.md` has the\ntable.\n\nIt has no dependencies either. The protocol is a `Content-Length` header, a blank line and a\nhandful of object shapes, so the JSON reader and the framing are written out. Two parts are\nworth reading. Positions: the protocol counts UTF-16 code units and the compiler counts\nbytes, which agree for ASCII and stop agreeing the moment somebody writes a comment in\nTurkish. And URIs: a space arrives as `%20`, a Windows drive as `/c%3A/`, and a Turkish\nletter as two escapes that are bytes rather than characters. Getting either wrong is silent.\n\n`deed debug` is the other half of that stream: the Debug Adapter Protocol has the same\nframing and the same JSON, so neither is written twice. What it needed that did not exist was\nsomewhere for a running program to be held still. The interpreter is recursive and single\npass, so there is no state machine to suspend, and there was no plan to write one: what it\nhas instead is a point before every statement where nothing is half done. It calls a watcher\nthere and carries on when the call returns, and **a watcher stops by not returning**. That is\nthe whole of suspension. The host stack is the program's stack, so the frames and bindings a\nclient reads are the ones the program is actually in, and nothing is re-run to reach them.\n\nThe interpreter decides nothing about debugging. It does not know what a line is. Breakpoints,\nwhat \"step over\" means, and when to carry on all live in `deed-dap`, because they are protocol\nquestions and putting them in both crates is how a debugger comes to stop somewhere the\ncompiler says is nowhere. Stepping is defined against the number of active calls: over is not\ndeeper than here, out is shallower, in is anywhere. Stepping into a `perform` lands in the\nhandler body with no special sentence attached, because an operation is a call and the stack\nalready says where it went.\n\nTwo things it does not do, both written down rather than left to be found. There is no\n`pause`: a session answers one message with the messages it caused, including running to the\nnext stop, so nothing is reading the client while the program runs. And there is no\n`evaluate`, so there are no watch expressions and no conditional breakpoints. Evaluating one\nmeans running Deed code inside a watcher, which is re-entering an interpreter that is\ncurrently lent out, and the shape that makes suspension free is exactly the shape that makes\nthat unsafe.\n\nThe examples are [transfer.deed](https://github.com/deed-lang/deed/blob/main/examples/transfer.deed),\n[counter.deed](https://github.com/deed-lang/deed/blob/main/examples/counter.deed), [hello.deed](https://github.com/deed-lang/deed/blob/main/examples/hello.deed),\n[config.deed](https://github.com/deed-lang/deed/blob/main/examples/config.deed), [todo.deed](https://github.com/deed-lang/deed/blob/main/examples/todo.deed),\n[journal.deed](https://github.com/deed-lang/deed/blob/main/examples/journal.deed), [logs.deed](https://github.com/deed-lang/deed/blob/main/examples/logs.deed),\n[proven.deed](https://github.com/deed-lang/deed/blob/main/examples/proven.deed),\n[closures.deed](https://github.com/deed-lang/deed/blob/main/examples/closures.deed), [diverge.deed](https://github.com/deed-lang/deed/blob/main/examples/diverge.deed),\n[strings.deed](https://github.com/deed-lang/deed/blob/main/examples/strings.deed), [lists.deed](https://github.com/deed-lang/deed/blob/main/examples/lists.deed),\n[generics.deed](https://github.com/deed-lang/deed/blob/main/examples/generics.deed),\n[generic_types.deed](https://github.com/deed-lang/deed/blob/main/examples/generic_types.deed),\n[using_list.deed](https://github.com/deed-lang/deed/blob/main/examples/using_list.deed), [calculator.deed](https://github.com/deed-lang/deed/blob/main/examples/calculator.deed),\n[ranking.deed](https://github.com/deed-lang/deed/blob/main/examples/ranking.deed),\n[kv_store.deed](https://github.com/deed-lang/deed/blob/main/examples/kv_store.deed), [json.deed](https://github.com/deed-lang/deed/blob/main/examples/json.deed),\n[stack_machine.deed](https://github.com/deed-lang/deed/blob/main/examples/stack_machine.deed), [tic_tac_toe.deed](https://github.com/deed-lang/deed/blob/main/examples/tic_tac_toe.deed),\n[markdown.deed](https://github.com/deed-lang/deed/blob/main/examples/markdown.deed), [scheduler.deed](https://github.com/deed-lang/deed/blob/main/examples/scheduler.deed),\n[tasks.deed](https://github.com/deed-lang/deed/blob/main/examples/tasks.deed),\n[tree.deed](https://github.com/deed-lang/deed/blob/main/examples/tree.deed), [generator.deed](https://github.com/deed-lang/deed/blob/main/examples/generator.deed),\n[workers.deed](https://github.com/deed-lang/deed/blob/main/examples/workers.deed), and the three that see\neach other: [names.deed](https://github.com/deed-lang/deed/blob/main/examples/names.deed), [sink.deed](https://github.com/deed-lang/deed/blob/main/examples/sink.deed) and\n[greeting.deed](https://github.com/deed-lang/deed/blob/main/examples/greeting.deed). All are checked by every pass on every commit,\n`hello.deed`, `config.deed`, `todo.deed`, `journal.deed`, `logs.deed` and `workers.deed`\nhave a `main`, and the rest run their own tests.\n\n`todo.deed` is the one written to find out what is missing rather than to show what is there.\nIt reads a list of tasks out of a directory it was handed, adds one or marks one done if it\nwas given anything on the command line, counts them, and prints the ones that are not done.\nThat is the smallest thing anybody would call a program and it was not writable at all a week\nago. It found four things. Three of its functions were the same function: start at zero, look\nat each element, stop when the index runs out, and declare `Diverge` for the privilege. An\naccumulator had to be threaded through as a parameter, because handler state is the only\nmutable thing in the language and reaching for a handler to collect strings would be using an\neffect to avoid a loop. Those two are what decided what a loop looks like here, and the three\nwalks are `for` loops now with nothing declared. The file format was `x|title` rather than\n`[x] title` because splitting was all there was, so the data got bent to fit the tool. And\nthe first run printed its own output backwards over itself, because splitting on `\\n` leaves\na carriage return on every line of a file written on Windows and there was nothing that\ntrimmed one off. The last two are what `trim` is for, and the file format is `[x] title` now.\nNone of those were obvious from inside the compiler.\n\nMarking a task done is the thing that file said for months it could not do, and it turned out\nto be one `map` over the tasks with one of them replaced. What took the time was being able\nto write that `map` once: generic functions, generic types and a row variable all had to\nexist first, and once they did the feature was four lines. It found one more thing on the way\nout, a small one. `state` was a keyword, so `with state = ..` did not parse, and `state`\nmeans something in exactly one position where the only alternative is `fn`. Reserving a word\nthat common for one position is a cost nobody had paid until a program wanted the word, so it\nis a name again and the parser recognises it where it matters.\n\nThe last thing on its list was two tasks with the same title, where `done buy milk` finishes\nboth because a title is being used as a name and it is not one. `done 2` finishes the second\ntask now, and no part of the language changed to allow it, which is what makes it worth\nreporting. A position is a fact about where an element is and a callback is only ever handed\nthe element, so `map` and `filter` stop being enough the moment position matters and the walk\ngoes back to a counter in a record written out by hand. There were three of those in that file\nwhen this was written, one of them replacing a `map(filter(..))` that used to be a single\nline. `for task at here in tasks` came out of exactly that and took all three back to one\nline each.\n\nAnd nothing bounds the number. `done 9` on a file with two tasks walks both, marks neither\nand hands back the list it started with, so whether it meant anything has to be asked again\nby a second function comparing it against the length. That is the shape an index has when the\ntype system cannot hold \"in range\", and it is the argument for the refinement tier made by a\nprogram rather than by a design document. What to do about it is the next question rather\nthan this one.\n\n`for` is a fold with syntax rather than a loop with a variable in it:\n\n```deed\nlet total = for n in numbers with sum = 0 {\n sum + n\n}\n```\n\nThe block's value is the accumulator for the next turn, and `sum` is a fresh binding every\ntime rather than something assigned to, so iteration exists and a handler's `state` is still\nthe only mutable thing in the language. The second reason for that shape is `Diverge`: there\nis no termination proving, so a function that can reach itself has to declare it may not\nreturn, and without a loop every walk over a list is recursion. A row that almost every\nfunction carries the same entry in has stopped saying anything. A `for` walks a list that is\nalready there, so it stops, so it declares nothing.\n\nIt also says where in the list it is, which came out of `todo.deed` for the third time.\n`for task at here in tasks with kept = []` binds the position, zero-based like the `at` that\nindexes a list, and it is known to be a real one: not negative, and below the length of what\nis being walked. Before it, three walks in that file carried a counter in a record so that\nsomething could ride alongside the answer, and every branch had to remember to bump it. The\nreason this is in the language rather than in the library is that the library cannot have it\notherwise: everything in `std/list` is written with a `for`, so `map` cannot hand a callback\nsomething the walk never knew. With it, `map_at` is four lines of Deed and no part of the\nlanguage grew a second `map`. `at` is still an ordinary name, since the only thing that can\nfollow a `for` binder is `at` or `in`.\n\n`journal.deed` is the half `todo.deed` could not write. `Io` could read a file and open a\ndirectory and there was no operation that wrote one, so `Dir` was a read capability wearing a\nmore general name. `Io.save` is that operation, and the thing worth looking at is what stops\nit writing anywhere else. Two separate things do. The row: a function that does not declare\n`uses Io.save` cannot write, whatever it is holding, so reading and writing are different\nauthorities over the same capability and which one a caller is handing over is written in the\nsignature. The capability: `Io.save` takes the `Dir` it writes into and there is no way to\nconstruct one, and the name goes through the same check reading goes through, so `..`, an\nabsolute path, a separator and a symlink pointing out are refused for writing exactly as they\nare for reading. Not a second implementation that agrees today.\n\n`Io.remove` is the case where a second kind of `Dir` was most tempting. Reading, listing and\nwriting all leave what was there; deleting does not, and a program that writes the wrong\nbytes can be put back from what it overwrote while one that deletes the wrong file cannot be\nput back from anything. It got the same answer as writing did, and for the same reason:\n`uses Io.remove` cannot be reached from `uses Io.save`, holding a `Dir` says nothing about\nwhich of the four operations a function may do, and nothing new had to be built for it. That\nis three tests of the same claim now, and the third was the one meant to break it. `todo.deed`\ncan say `clear`, and the function that does the deleting declares `uses Io.remove` and\nnothing else, so it cannot read the file it is about to delete.\n\n`Io.make` is the fourth test and the one that looks like it breaks the rule that authority\nonly ever shrinks. It hands back a `Dir`, and a `Dir` is authority, so this document said for\na while that creating a directory was authority being made rather than narrowed. That was\nwrong. A `Dir` reaches everything under its root and which of those paths happen to exist is\nnot part of what it grants, which is why `Io.save` writing a file that was not there is not\nauthority creation either. What `Io.make` returns is rooted inside what it was given, so it\nreaches strictly less, and there is a test that makes a directory and then fails to climb out\nof the result. Nothing may already be at the name: \"I made it\" and \"it was already there\" are\ndifferent answers.\n\n`Io.epoch` is the same split about something other than authority. `Io.now` counts calls\nrather than reading a wall clock, because P8 says the default is deterministic and a real\nclock would make every run different, which is the right answer for a test and the wrong one\nfor a program that needs the actual time. So the machine's clock is a second entry in the\nrow on the same `Clock`. `uses Io.now` cannot reach it and it cannot reach `uses Io.now`,\nand what that buys is not narrower authority: a signature saying `uses Io.epoch` is a\nfunction whose output can change between two runs of the same program, and that is now\nsomething you can see without reading the body.\n\n`workers.deed` is the one written to find out what concurrency cannot say. Several workers\nread different directories and one collector writes a report. The workers declare\n`uses Io.list, Io.read` and the collector declares `uses Io.save`, and neither can do the\nother's job: a worker that was never handed `Io.save` cannot write, and a collector that\nwas never handed `Io.list` or `Io.read` cannot list or read, whatever `Dir` they happen to\nhold. Both of those facts are checked rather than stated in a comment. What the program\ncannot say is what the walls produced: there is no spawn, so the workers run one after\nanother even though their authorities are disjoint; there is no channel, so a worker cannot\npush results to the collector as it runs; and the type system cannot prove that two `Dir`\nvalues name directories that do not overlap.\n\n`proven.deed` is the one that argues with itself. Every function in it either proves its\npostcondition or explains, in a comment, why the checker cannot, and the file is written so\nthat the two halves sit next to each other. The `Proven` tier used to hold constant\nexpressions and nothing else, which made a refinement in real code a runtime check with\nceremony around it. It now reasons about intervals, about the difference between two names,\nand about what a callee promised: a `where` clause, a refined parameter type, an `if`\ncondition, a guard that returns, `low < high`, and `ensures ok => result == n` at a call site\nare all facts the rest of the body can use.\n\nHow long something is is one of them now. `length(items)` used to come back as a range and\nnothing else, which meant it could not be one side of a difference, so `index < length(items)`\nwas invisible to the machinery that existed for `low < high`. A length is a term keyed on the\nthing being measured, and the rest falls out of the two rules that were already there: the\ndefault is zero and up, because there is no list with fewer than no things in it, and past\n`if length(items) <= 0 { return err(..) }` one less than the length is an index that is really\nthere. Two lists are two terms, and `length(f(items))` is not a term at all, since two calls\ncould hand back two different lists.\n\nThat was prompted by `todo.deed`, which marks a task by position now and could not say no to\n`done 9` before running. What made the fact worth having is the other half of the same\nchange: a `where` clause is read at the call site now. It was not before. A precondition was\na fact for the callee's body and a check inside the callee at runtime, and nothing ever\nlooked at it from where the call was written, so `halve(0 - 5)` against `where n >= 0` passed\nthe checker in silence. The design doc had described the call-site check for months. Now a\ncall that plainly breaks a clause is an error where the call is, a caller that can show the\nclause holds is `Proven`, and a caller that cannot is `Guarded` with the runtime check still\nstanding. `proven.deed` went from four proven obligations to forty-five that way, and most\nof them are calls rather than values.\n\nWhat crosses into a clause is the caller's facts said in the callee's parameter names: each\nargument's range, how long it is, and the differences between them. That last part is what\nsettles `index < length(items)`, which is the clause the whole detour was about. The clause\nitself crosses a module boundary whole, unlike a refinement predicate, because a refinement\nis a proof the declaring module already did and a precondition is a question only the caller\ncan answer. What travels with it is what each name in it refers to, worked out where it was\nwritten, since a clause's spans are offsets into that file and nowhere else.\n\nA refinement could say the same thing about a length and could not be settled, which is the\nkind of gap you only find by writing the two side by side. `value` has no declaration of its\nown, so it travelled as a range, and a range answers `value > 0` and cannot answer\n`length(value) > 0`: that is a question about a term and a term needs something to be keyed\nby. So `if length(s) > 0` proved a `where` clause saying `length(s) > 0` and left a refinement\nsaying the same thing Guarded, over the same fact, two lines apart. A value being checked now\ncarries what is known about it three ways, the range it lands in, how long it is, and the name\nit was given when it has one. The name is the strongest of the three, since it is the entry\nthe body has been narrowing all along. The length covers the case with no name to give, so\n`\"\"` where a non-empty string is wanted is refused outright instead of being left to a check\nat runtime, and a string written on the spot proves the refinement it is being passed into.\n\nThe same thing was missing from both of the other directions, which is what a gap like that\nusually turns out to mean. A parameter already of a refined type is a fact without a `where`\nclause repeating it in prose, and that held for what the value is worth and not for how long\nit is, so a `NonEmptyList` knew nothing about its own length inside the body that declared it.\nAnd narrowing into a refinement asked for the base type exactly rather than asking the\nquestion the base type would have been asked, so `first_of([])` came back as \"expected\n`NonEmptyList`, found `List<_>`\". The empty list fits a `List` perfectly well. What is\nwrong with it is the predicate, and that is what it says now.\n\nThat also answered a question the design doc had listed as open. A refinement has no\nconversion form, and it turns out not to need one: `try_positive(n)` returning a `Result` is\nwhat `Positive.try(n)` would have been, it is ordinary code, and the `ok` is Proven because\nthe guard above it says what the predicate wants. What a built-in form would buy is the\npredicate living in one place rather than being restated at every converter, and a\nrestatement weaker than the predicate is the mistake it would rule out. That one is still\naccepted today with a runtime check rather than refused, which is honest and is not the same\nthing as catching it.\n\nIt still does not finish the job. `at` returns a `Result` whatever is known about its index,\nso a caller that proved the bound still writes a `match` for a failure that cannot happen.\nA total indexing form is a precondition on a prelude function, which is a thing the language\ncan now express, and whether the prelude should carry one is a question rather than an\noversight.\n\nIt also used to refuse `n + 1` on a `Positive`, and this paragraph used to say that was the\nreasoning working. It was not. Overflow is an error rather than a wrap, so `n + 1` either\nproduces a value or stops the program, and it never produces a wrong one; so a value that\nexists is inside `Int`, and any sum that exists is greater than one. The interval clamps at\nthe edge instead of collapsing, and the runtime check that used to be emitted there could\nnever have fired. Two of the three warnings in the file went away and the comments explaining\nthem turned out to be the more interesting half of the fix.\n\nWhat it still cannot do is relate two names through a product, so `result == n * n` says\nnothing. [design/02-syntax.md](https://github.com/deed-lang/deed/blob/main/design/02-syntax.md) lists the rest.\n\n`transfer.deed` used to model something that could not exist. `Money.units` was `Positive`,\nwhich made a zero balance and a debit unwritable, and the type checker said so. The fix was\nto separate the type that can be zero from the type that cannot, which is the sort of thing\nthe language is supposed to force and did.\n\n`hello.deed` was worse. The test written to prove that a function without a `Console` cannot\nwrite to one failed, because `Io.write(Console, \"hi\")` type checked: a type name in\nexpression position had no type, and no type agrees with everything. Capability safety was\ndecorative for about an hour. That is now `DEED4019`.\n\n`closures.deed` is the same shape of bug found twice in one place. A parameter could be\nwritten with no type, which made it the unknown type, and a closure's effects were charged to\nnobody. Either alone is arguable. Together they meant a closure could carry any effect into\nany function with the row staying empty the whole way. A parameter now needs a type, and a\nclosure's effects are charged to whoever wrote it. A closure can leave the function that\nwrote it, and the type it leaves through says what it may do on the way: `Fn(Int) -> Int`\nperforms nothing, `Fn(Int) uses Log.note -> Int` performs that and no more. Leaving a row off\ncannot mean any row, or a value could carry an unstated effect through a signature.\n\n`diverge.deed` is what a design document claiming something the compiler did not do looks\nlike when it gets fixed. \"Non-termination is an effect\" had a section of its own and\n`Diverge` appeared nowhere else in the repository, so the word did not even resolve. Running\nan unbounded recursion overflowed the host stack and killed the process, with no diagnostic\nand no exit code anyone could read. Now a function that can reach itself has to declare it,\nmutual recursion included, and the interpreter reports `DEED6009` instead of dying. There is\nstill no termination proving, so `factorial` has to declare it too, and the design document\nsays that rather than hoping.\n\n`strings.deed` exists because until recently there was no way to join two strings. A program\ncould not build a message out of pieces, so nobody could write a program, so every other\ndecision here was untested. Fixing it turned up the same bug from the other side: `<` was\naccepted on anything as long as both sides had the same type, so comparing two records passed\nthe type checker and failed at runtime with a message blaming the interpreter for not\nimplementing something that has nothing to implement. It now also carries `split`, `join`,\n`to_string` and `to_int`, which are two pairs of inverses and are there for one reason: a\nprogram could hold text and hold a number and get from neither to the other, so it could not\nread input, print a count, or write anything back out.\n\n`lists.deed` is the same complaint one size up. Until it, nothing in the language could hold\nmore than one of something, so every program was one that worked on a fixed number of named\nvariables. `List` is built in rather than declared, and it is the same shortcut `Result`\ntakes: element types are compared componentwise and an unknown one absorbs, so `[]` fits\nwherever a list was wanted and no\nunification was needed anywhere. What the file is honest about is iteration: at the time\nthere was no `for`, so walking a list was recursion and every walk declared `Diverge`. That\nwas not an oversight. An accumulator loop wants mutation or a fold, and mutation here is\nsupposed to be handler state and nothing else, so the shape of `for` was an argument about\nthe central claim of the language rather than a piece of syntax to add.\n\n`generics.deed` is what the two shortcuts were actually costing. Not the shortcuts: nobody\ncould write a library. `first`, `last`, `map` and `count_where` are one function at different\nelement types and none of them could be written down anywhere in this repository. A generic\nfunction costs this design almost nothing, because there is still no unification: at a call\nsite the declared parameter types are matched against the argument types, walking down both\nin step, and `List` against `List` gives `T = String`. One rule carries the rest.\nEvery type parameter has to appear in a parameter's type, which means a call always knows\nwhat every parameter is, which means no type arguments are ever written, which means\n`f(b)` versus `f < a > (b)` is not a problem this parser has. It is also the same claim\neverything else here makes: a signature is complete.\n\n`generic_types.deed` is the other half, and it is where the shortcut stops being one.\n`Option` was always the third generic type people reach for, and it is declared there rather\nthan built in. A generic type is a head plus arguments compared componentwise, which is\nexactly how `Result` and `List` were already compared, so the mechanism was half built\nbefore it was asked for. What decides the arguments is the same matching a call does: a\nliteral matches its declared field types against the values it was given. A field then reads\nat the type it was applied to, and so does a pattern binder, which is the part a test caught:\n`Some { value }` on an `Option` has to bind an `Int` rather than the `T` the choice was\ndeclared with.\n\n`std/list` and `using_list.deed` are the point of the three changes above. `std/list` is a\nlist library written in Deed: `map`, `map_at`, `filter`, `filter_at`, `fold`, `fold_at`, `any`,\n`all`, `count_where`, `filtered_with`, `first`, `last`, `reversed`, `prepend`, `find`, `take`, `drop`, `concat`, `flatten`, `partition`, `zip`, `enumerate`, `windows`, `chunks`, `intersperse`, `unzip`, `flat_map`, `scan`, `transpose`, `group_by`, `sort`, `sum` and `largest`, none of them known to the\ncompiler, no builtin, no special case, no name in the prelude. It is the first thing in this\nrepository anybody else could have written.\n\nIt ships with the compiler, and it did not always. It sat under `examples/` for months, and a\nmodule's name says where it lives, so the only way to import it was `use examples/list` and a\nprogram written anywhere else had to copy the file. Nothing about the library changed when it\nmoved.\n\nIt is also what got the language a way to stop a walk. `any` and `all` in it both used to\nopen with a branch whose only job was to notice that the answer was already in, which is\ncontrol flow inside a fold, which is the thing a fold exists to not have, and the branch could\nskip the work but not the turn. The design doc said `break` and `continue` had not come up in\na program written here, and this file was the counterexample sitting in the repository. So a\n`for` takes a `while` now, read before each turn with the accumulator in scope and the element\nout of it, since the element belongs to the turn the condition is deciding whether to take.\nBoth functions lost their branch. It is not `break`: nothing is abandoned, the value of the\nloop is the accumulator it stopped holding, and the list still bounds how many turns there can\nbe, so the termination argument that keeps a `while` statement out is untouched.\n\nPointing `todo.deed` at it found the last thing missing. The compiler only looks at the files\nit was handed, which is a rule worth having, and it meant `deed run examples/todo.deed` could\nnot find the library and the workaround was to name every file the program transitively\nneeds. A library nobody can use without knowing its file layout is not a library. A module's\nname says where it lives now: a module named `a/b` is at `/a/b.deed`, and the root comes\nfrom taking a named file's module path off the end of its own path. No search path, no config\nfile, no manifest, and it is a rule every file here already followed.\n\nWhat was named is the subject and what an import needed is context, so `deed test app.deed`\ndoes not run a library's tests and `deed check app.deed` does report a library's errors. That\nis the same split the language server already makes between the workspace and the open\ndocument.\n\nWhat `std/list` needed last was a row variable. Before that there were two ways to write\n`map` and both were wrong: `Fn(A) -> B` promises to perform nothing, so the callback could\nnot log or read a file, and `Fn(A) uses Log.note -> B` works for one effect and needs a\nsecond copy for the next one. `uses r` stands for whatever the callback performs and passes\nit through to the function's own row, so `map(ns, |n| n + n)` performs nothing and\n`map(ns, |n| { Log.note(..); n })` performs `Log.note`, and the second caller has to say so.\nThe library says \"whatever you gave me\" and the caller says what that was.\n\nInside the body a row variable is an ordinary entry: calling the callback performs `r`, the\ncontract says `uses r`, and the same two rules that check every other function check that\none. Which is why a variable that reaches no parameter was already an error before anything\nwas written for it, since nothing can fill it, so nothing performs it, so the row is too wide.\n\nThe design doc spent a while listing \"can a row variable appear in two parameters\" as an open\nquestion, on the assumption that the second occurrence was checked against the first the way\na type parameter's is. Measuring it first said otherwise: nothing compares them, and the call\nsite unions the row of every argument the variable came from. That is the useful answer, so\n`filtered_with(ns, keep, dropped)` takes a pure `keep` and a `dropped` that logs and charges\nthe caller `Log.note`. A variable is not a name for one row that every parameter carrying it\nhas to agree on, it is a name for the places a call reads a row off. The behaviour was right\nand untested, which is a worse position than being wrong and tested, so it is pinned now.\n\nLooking at that machinery again turned up a hole that had been open the whole time. The\npass worked out a function value's row by matching on the shape of the expression: it knew a\nclosure written on the spot and a bare name, and answered \"performs nothing\" for everything\nelse. An empty row is a claim rather than an absence, so every other shape was a claim nobody\nhad checked, and there were five of them. A function that came back from a call, one chosen\nby an `if`, one taken out of a list, one read out of a record field, and a call applied\nstraight to the result of another call. Each one ran an effect through a caller that declared\nnone, and the argument in the comment for why that was safe confused two different questions:\nwhether a value performs more than its type allows, which was checked, and what calling it\ncosts the caller, which was not.\n\nThe row is part of the type, and the type checker already works out a type for every\nexpression, so it hands over the row of every function-typed one and the guessing is gone.\nThe rule that had to come with it is where a row variable may be written: the row of a\nparameter that is a function type, and the declaration's own `uses` clause, and nowhere else.\nA variable in a return type reaches a caller standing for something that caller has no word\nfor, so it gets dropped, and a dropped entry is an effect that happens and is not declared.\nThat is the same rule as the one saying a type parameter has to appear in a parameter's type,\nand for the same reason: a signature whose call sites cannot work out what it means is not a\nsignature.\n\nFive holes in one place, all found by hand, is a bad way to find out. So the interpreter\nholds the program to its own signatures while it runs. Each active call carries the row its\ndeclaration wrote down, every effect performed is checked against every call on the stack,\nand one nobody declared is an error reported against the compiler rather than the program,\nsince the file was accepted and so the check that accepted it was wrong. A `with` block\ndischarges what is inside it and a contract does not contribute to a row, so both are exempt,\nwhich are rules the language already had rather than allowances made here. Pointed at\n`examples/`, it passes, and with the fix above taken back out it fails on the first program\nthat used to slip through. The point is not what it finds today. It is that the next one\nreports itself, with a stack, from a real program.\n\nIt found one the same day it was written, which is sooner than I expected and worse than I\nexpected. A `with` block discharges the effect the handler implements, which is what a\nhandler is for, and it said nothing about what the handler does to implement it. So a\nfunction handed a `Console` could install a handler whose operation writes to that console,\nrun it, and declare an empty row. Everything checked clean and the screen still got written\nto. Those effects go to whoever installed the handler now, which is the function that made\nthe decision, and a handler carries what it performs across a module boundary the same way a\nfunction carries its row.\n\nThe worst one so far was found the same afternoon. The `Guarded` tier did not guard a return\nvalue. `deed check` printed \"so it becomes a runtime check\" and there was no check: the\ninterpreter guarded arguments and annotated `let`s, because those were the two places\nsomebody had happened to write the call. A function declared to return a `Positive` would\nhand back a `-5` and every caller downstream was entitled to believe it. The warning was the\npart that made it dangerous, since that is what convinces a reader they are covered. The two\npasses now read the same table, and `crates/deed-driver/tests/guards.rs` has a test for every\nplace a refined value can come into existence, each one handing the guard something it is\nsupposed to refuse. The test that should have caught this did exist, and it passed, because\nit only ever handed the guard values it accepts.\n\nThose tests all had to be written in Rust, which was itself a gap and `proven.deed` said so in\na comment for months. A contract failure ends the run, so a file of examples showing a guard\nrefusing something could not pass, and then preconditions started being read at the call site\nand the checker began refusing such a file outright. The better the checking got, the further\nout of reach the check itself went. `assert refuses order_of(0)` says it from inside the\nlanguage now: it passes when a `where` clause, an `ensures` clause or a refinement turns the\nvalue down, and fails when anything else happens, including the call producing a value. That\nis the one thing in the language that catches, and it catches those three and nothing else,\nbecause overflow and a missing handler are a program going wrong rather than a signature\ndoing its job.\n\nThe `Tested` tier had a quieter version of the same problem. `deed test` generates a hundred\ninputs from a contract and shrinks whatever fails, and for a while it only shrank integers\nand the fields of records. So a counterexample of `[95]` came out when `[1]` says the same\nthing, and a variant would shrink its field to zero and stop rather than becoming the\n`Nothing` sitting next to it. A counterexample built out of something that does not shrink\nlooks exactly like a small one that happens to be awkward, and nothing tells you which it\nwas. Everything the generator can build shrinks now: lists get shorter before their elements\nget smaller, strings get shorter and then plainer, `true` gives way to `false`, and a variant\ngives way to a sibling that carries no fields. That last one is the only part that cannot be\nread off the value, so the choices are walked once and every variant is told which of its\nsiblings are empty.\n\nFive of these have now had the same shape: something has no type, the unknown type agrees\nwith everything, and checking quietly stops. So there is an invariant for it now. In a file\nthat checks cleanly, no expression is unknown, because an unknown one is an expression nothing\ndone with it was checked against. Written as a test and pointed at the examples, it found two\nmore in the first run and a third once those were fixed: closure bodies, handler literals, and\nevery call to an imported effect's operation. `crates/deed-driver/tests/fully_typed.rs` is\nwhere the next one gets found on purpose.\n\nLooking for the same shape one level up found the biggest one. A function's effect row did\nnot cross a module boundary, so every call into another file was free, and in a program with\nmore than one file that is most calls. The pass this language exists for was doing its work\non the calls that mattered least. Rows travel now, and a caller that inherits an effect it\nnever imported is told which module to import it from, because a row that cannot name what it\ngrants is not a row.\n\nThe grammar had one of its own. Statements are separated by nothing, so what ends one is the\nnext token not being able to continue the expression before it, and the design doc said that\nheld only by coincidence. It did not hold at all: `(` starts a parenthesised expression and\ncontinues a call, `-` starts a negation and continues a sum, so `let a = 1` with `-2` under\nit read as `let a = 1 - 2` and the second line was gone with nothing said about it. A line\nbreak ends an expression now, and the rule is the same inside brackets as outside them,\nbecause a rule that switches off somewhere is a rule people have to remember. Nothing\ncanonical changes shape under it, since `deed fmt` never breaks a binary expression across\nlines.\n\nBeing right is half of it. The rule makes a new mistake possible, which is carrying an\noperator down to the next line, and both halves of that are answered. `* 2` on its own line\nis a parse error that says why rather than only what, and takes the rest of the line with it\nso one mistake gets one complaint. `- 2` on its own line is a perfectly good expression and\nthere is nothing to refuse, so what is left is a statement whose value nobody reads, and\nsaying that is `DEED4026`. It is a warning, because `let _ = f()` is how a program says it\nmeant to throw a value away and working code should not have to be rewritten to keep\ncompiling, and dropping a `Result` gets its own sentence, since that one loses the failure\nrather than a line.\n\nThen the escape hatch turned out to have a hole. `let _ = f()` throws the value away and\nsays so, but `let b = f()` silences the warning too, and now there is a name nobody reads,\nwhich is the same statement doing nothing with an explanation attached. So a `let` binding\none plain name that no expression mentions is `DEED3009`. The measurement is the interesting\npart: pointing it at every binder fired twenty seven times across the examples and twenty\nfive of those were not mistakes, because a pattern is there to match and `err(why)` names\nwhat the shape holds, a parameter's shape is the signature and a handler's belongs to the\neffect it implements, and a `for` binder walks whether or not the element is wanted. A `let`\nis the one form whose entire reason for existing is the name. Narrowed to that, it fires\nonce in the whole corpus, on a binding an example had already called `unused`.\n\n`deed fmt` prints one canonical form and takes no options for the output. P4 said formatting\nis not configurable long before anything enforced it, which meant the files were formatted\nthe way they happened to have been typed. A test now asserts that every `.deed` file in the\nrepository is already canonical, so the principle either holds or the build fails.\n\n`deed fix` is the same move for P7. Diagnostics already carried a patch and a note about\nwhether that patch is certain or a guess, and nothing applied them, so what P7 described was\na data structure. `deed fix` applies the certain ones and refuses the guesses, with no flag to\noverride that. Which left the guesses reachable by nothing, and the certain ones reachable\nonly from a place the reader has already left, until the language server started offering\nboth as quick fixes.\n\nIt writes rows now, which is the part that costs something day to day. A fix is a span and a\nreplacement, so most of them are handed over where the problem is found, and the row\ndiagnostics could not: `DEED5001` names the effect, names the function and tells you to add it\nto the `uses` clause, and saying that as a span means knowing about commas, about indentation,\nand about a clause that may not be there yet. The effect checker has the answer and no\nbusiness knowing any of that, so the driver writes those, where the text, the tree and the one\ncanonical layout are all in scope. `deed fix` fills in a row that is too narrow, takes out an\nentry that is never performed, and what it writes is exactly what `deed fmt` would have.\n\nIt declines twice, and both are the point. A contract holding a `where` or an `ensures` is\nleft alone, since the region between a signature and its body holds all three and nothing in\nthe tree says where one stops and the next starts. And a comment anywhere in that region stops\nit, because rewriting the block would eat the comment, and a machine-applicable fix that\ndeletes a comment is a fix nobody should have applied.\n\nAn unused import goes the same way, one pass earlier. `DEED3003` knows which name nothing uses\nand knows nothing about the comma beside it, and taking the last name out of a list is a\nquestion about a line and the blank line next to it. One fix for the whole block rather than\none per name, which is not tidiness: two names out of the same list are two edits over\noverlapping text and both get dropped, and two whole lines removed separately each leave\nbehind the blank that used to sit beside them, so the file ends up with a gap that no longer\nseparates anything. Rewriting the block once has neither problem, and what it writes is what\n`deed fmt` would have.\n\nThe two warnings about something going nowhere carry a guess each, and a guess is what the\neditor is for. `DEED3009` offers `_spare`, `DEED4026` offers `let _ = ` in front of the line,\nand neither is ever applied in bulk, because the other way to arrive at either one is a value\nthat was supposed to be read and papering over that is the single thing they must not do.\n`DEED4026` is also the first fix the type checker has ever carried. A type that does not fit\nhas no obvious repair, which is why there were none, and this one has exactly one mechanical\nanswer that is still not certain to be what was meant.\n\n`deed check --timings` is the same move for P9, which said check latency is budgeted and had\nnever been measured. The guard is not a wall clock budget, since a test that fails on a busy\nmachine is a test people learn to rerun. It is the shape of the curve: ten times the input\nhas to cost well under a hundred times the time. That test found a quadratic on its first\nrun, in the \"did you mean\" suggestions, which cost an edit distance against every name in\nscope for every name that failed to resolve.\n\n`names.deed` and `greeting.deed` are two modules that see each other. A module is named by its\nown `module` line, and the unit of compilation is the set of files you handed the compiler,\nso `deed check examples/` resolves the `use` in one against the declarations in the other. A\n`use` of a module that is not there is an error, so is a name it does not declare, so is a\nfield an imported record does not have, so is a `match` on an imported choice that forgets a\nvariant. None of that was checked before: an imported name had no type, and a name with no\ntype agrees with everything, so a module boundary was a place where checking stopped.\n\nRunning crosses it too. A call through an import walks into the other module's body with\nthat module's own names in scope, and a variant carries the module that declared it, so the\nsame variant reached two ways is one value. Effects cross as well: `sink.deed` declares an\neffect and two handlers, `greeting.deed` performs the effect and installs the handlers, and\nthe row is checked against the declaration in the other file in both directions.\n\nNo dependencies. `cargo test` runs the whole thing, and one of the tests is that\n`examples/transfer.deed` survives every pass.\n\n`deed check` runs every pass even when an earlier one failed. Stopping at the first failure\nwould cost a round trip for everything the later passes would have found, and the design\nmakes running on safe: parse errors become error nodes, unresolved names become unknown\ntypes, and unknown agrees with everything. Diagnostics come out in source order rather than\npass order, because a reader works down the file and which pass noticed is not their problem.\n\n## What Deed is deliberately not doing\n\nNo macros, no inheritance, no exceptions, no operator overloading, no implicit\nconversions, no optional syntax. Each of those makes a function impossible to understand\nwithout reading something else, which is exactly the cost this language exists to remove.\n\nDeed is less pleasant to write by hand than most modern languages. That is the trade, made\non purpose.\n\n## The obvious problem\n\nThere is no training data for a language nobody has written yet, and no ecosystem either.\nThe only real answer to the first is to keep the specification small enough to read in\nfull, in one sitting, so the language never has to be remembered. That is a hard\nconstraint on the design, not a nice-to-have. The answer to the second is interop, and it\nis not solved yet.\n\nIf you think there is a better answer, please open an issue.\n\n## Contributing\n\nSee [CONTRIBUTING.md](https://github.com/deed-lang/deed/blob/main/CONTRIBUTING.md). Short version: the design is the thing that needs\nattacking right now, not the code.\n\n## License\n\nLicensed under either [MIT](https://github.com/deed-lang/deed/blob/main/LICENSE-MIT) or [Apache-2.0](https://github.com/deed-lang/deed/blob/main/LICENSE), at your option.\n","changelogMarkdown","videoKey","requiredSecretsJson","publishedAt","priceCents","trialDays",0,"iconType","image","upstream",{"_107":108,"_109":110,"_102":111,"_112":113,"_114":115,"_116":117},"requiredSecrets",[],"tags",[96,97,21,98,99,100,101,102,103,104,105,106],"assets",[],"stats",{"_94":81,"_95":81},"ratingAvg","reviewCount","capability-based-security","compiler","deedlang","design-by-contract","effect-system","interpreter","language","programming-language","refinement-types","rust","type-checker","topics",[96,97,21,98,99,100,101,102,103,104,105,106],"license","Apache-2.0","Rust","registryName","io.github.deed-lang/deed","homepage","https://deed-lang.github.io/agents/","packages",[118],{"_119":120,"_121":19,"_71":72},"registryType","cargo","identifier","ENV",{"_124":125,"_126":127,"_128":129},"ENVIRONMENT","production","TURNSTILE_SITE_KEY","0x4AAAAAAB8-rEI2gNDf_QhU","SENTRY_DSN","https://45fd1229f78089d5c3ee78be128030e1@o4510583261757440.ingest.de.sentry.io/4510584253448272"]