From 026f58f3d6cf3db2666781077cbb3480e6068efa Mon Sep 17 00:00:00 2001 From: onatozmenn Date: Sun, 9 Aug 2026 14:21:32 +0300 Subject: [PATCH] A page for the argument the language is built on `deed mcp` was one paragraph on the install page, which is the wrong place: a person deciding whether to wire a compiler into an agent is not reading a download page. This is that paragraph turned into somewhere to be pointed at. Everything it claims about what an agent receives, it demonstrates. The four transcripts are filled in from the pinned artifact in the reader's tab, for the programs printed above them, so nothing on the page is a sample output written here. That rule already covers the playground and the diagnostics index; it matters more on a page whose whole subject is what a machine gets back. What they show, in order: - an obligation line carrying a tier, `proven` and `tested` in the same answer, neither of them asked for; - the same refinement without the precondition that establishes it, coming back `guarded` with a reason a model can act on; - the `export` diagnostic, with a machine-applicable edit and the note saying why the word does not exist, which was the single most common thing said across five recorded runs; - `deed_test` running a property generated from a contract, in a module with no tests in it. The benchmark is here as a table with the control arm beside it, and as a link to the record rather than a copy of it, along with the three things it does not establish. A page that quotes a measurement without its caveats is worse than one that quotes nothing. `assets/agents.js` carries the same `TAG` and `VERSION` as the other two scripts, so `tools/check.mjs` holds it to the pin like the rest. Nav gains a sixth entry on all six pages, and the landing page a fourth card. --- README.md | 1 + agents/index.html | 238 ++++++++++++++++++++++++++++++++++++++++++ assets/agents.js | 149 ++++++++++++++++++++++++++ errors/index.html | 1 + index.html | 8 ++ install/index.html | 1 + one-clause/index.html | 1 + play/index.html | 1 + 8 files changed, 400 insertions(+) create mode 100644 agents/index.html create mode 100644 assets/agents.js diff --git a/README.md b/README.md index 863d849..8b26c56 100644 --- a/README.md +++ b/README.md @@ -121,6 +121,7 @@ checked through the pinned artifact and every one of them is clean. ``` index.html what the language is play/ the playground +agents/ what `deed mcp` hands back, asked in the tab errors/ every diagnostic code, read out of the compiler install/ how to get a binary running one-clause/ what a signature turns into diff --git a/agents/index.html b/agents/index.html new file mode 100644 index 0000000..7dddf3c --- /dev/null +++ b/agents/index.html @@ -0,0 +1,238 @@ + + + + + + For agents | Deed + + + + + + + +
+
+
+
+

+ Deed +

+

A function can only do what its signature admits to.

+
+
+
+ + + +
+

For agents

+

+ Most code being written now is not typed out by a person. Deed is + built on that being true, and deed mcp is the part of it + you can point a tool at: a Model Context Protocol server, so the + thing writing the code asks the compiler instead of remembering. +

+

loading the compiler

+ + + +

What comes back that a type error does not

+

+ A compiler that only says yes or no tells an agent whether it has + finished. Deed says which of the promises in the signature it + settled, and which it could only arrange to check at + runtime. That is a gradient, and something iterating on its own + output can climb it. +

+ 
…
+ 
…
+

+ proven means the checker discharged it at compile time. + tested means it produced a property and ran it. Neither + was asked for. +

+ +

And when it cannot

+

+ The same refinement without the precondition that establishes it. The + answer is not "no", it is which tier this landed in and the reason it + did not land higher. +

+ 
…
+ 
…
+

+ Nothing narrowed this name is a sentence a model can act on. + It says where to look, which is the caller's side, and it is the + difference between a warning and a next step. +

+ +

A repair, and the reason behind it

+

+ Models reach for export, because most languages have one. + Across + five recorded runs + this was the single most common thing said, forty-five times, in + every task. So the answer carries the edit that fixes it and the + reason the word does not exist: +

+ 
…
+ 
…
+

+ machine-applicable is the compiler saying this one may + be applied without asking. Guesses are marked differently and are + never applied on their own, which is a distinction an agent can only + respect if it is told. +

+ +

A test nobody wrote

+

+ The contract in a signature is not documentation. Ask the same server + to run the tests of a module that contains none, and it runs the + property the contract generates: +

+ 
…
+ 
…
+

+ A hundred cases, from a seed that is in the answer so the run can be + repeated. In the recorded runs this happened three times to a model + that had been told not to write tests. +

+ +

Wiring it up

+

+ The server speaks MCP on stdin and stdout, so a client starts it the + way it starts any other: +

+ 
{
+  "mcpServers": {
+    "deed": { "command": "deed", "args": ["mcp"] }
+  }
+}
+

+ There is nothing else to install; see + Install. Six tools: + deed_check, deed_test, + deed_run, deed_fmt, deed_fix + and deed_explain. The full walkthrough is + in the repository. +

+ +

What it is not allowed to do

+

+ The server holds no capability. A program arrives as text and the + answer leaves as text; it opens no file, resolves no path, and + refuses to run a program whose signature reaches for a directory + before running a single instruction. That is not a sandbox bolted on + — it is the same rule the language is about, applied to itself. +

+

+ The cost is written down rather than hidden: a server with no + filesystem cannot be handed a module set, so a program that imports + another module has to arrive with it. +

+ +

Does it actually help?

+

+ Measured, not asserted. Six tasks, one model, five runs, against a + control arm with the compiler taken away: +

+ + + + + + + + + + + + + + + + + + + + + + + +
ArmAnsweredCheckPass their tests
prompt only6/600
with deed mcp6/65 or 65
+

+ Six confident answers either way, and not one of the prompt-only ones + compiles. Deed is in nobody's training data, which is what makes the + control arm worth having and what makes the number honest rather than + impressive. +

+

+ The record says what it does not establish, too: one model family, no + comparison against a language without contracts, and a control arm + recorded against an earlier build. + Read it + before quoting it. +

+
+ +
+

+ The transcripts on this page are what the pinned compiler answered in + your tab, for the programs shown above them. Nothing here is a sample + output written by hand. On the wire each answer is one JSON object per + line; the indentation is the only thing this page adds. +

+

+ Apache-2.0. This page has no analytics, no cookies and no third-party + requests. +

+
+
+ + + + diff --git a/assets/agents.js b/assets/agents.js new file mode 100644 index 0000000..0130b83 --- /dev/null +++ b/assets/agents.js @@ -0,0 +1,149 @@ +// The agent page's transcripts, asked of the compiler rather than written here. +// +// Every JSON line this page shows is what the pinned artifact answered in this +// tab, for the program printed above it. That is the whole point of the page: +// a claim about what an agent gets back is worth nothing if the page is the +// one making it up. + +const TAG = "v0.2.9"; +const VERSION = "0.2.9"; +const WASM_URL = `../assets/deed-${TAG}-wasm32-unknown-unknown.wasm`; + +const STATUS = document.getElementById("status"); + +// Each one is a program and the verb an agent would send it to. The programs +// are short on purpose: this page is about the answer, not the program. +const ASKS = [ + { + id: "tiers", + verb: "deed_check", + source: `module inventory + +type InStock = Int where value > 0 + +fn take_one(count: InStock) -> Int + ensures + ok => result >= 0, +{ + count - 1 +} + +fn restock(count: Int, delivered: Int) -> InStock + where + count > 0, + delivered >= 0, + count < 1000000000, + delivered < 1000000000, +{ + count + delivered +} +`, + }, + { + id: "guarded", + verb: "deed_check", + source: `module inventory + +type InStock = Int where value > 0 + +fn restock(count: Int, delivered: Int) -> InStock { + count + delivered +} +`, + }, + { + id: "repair", + verb: "deed_check", + source: `module inventory + +export fn restock(count: Int) -> Int { + count + 1 +} +`, + }, + { + id: "property", + verb: "deed_test", + source: `module inventory + +fn twice(n: Int) -> Int + where + n > 0 - 1000000000, + n < 1000000000, + ensures + ok => result == n + n, +{ + n + n +} +`, + }, +]; + +function esc(text) { + return String(text) + .replace(/&/g, "&") + .replace(//g, ">"); +} + +async function load() { + let wasm; + try { + const module = await WebAssembly.instantiateStreaming(fetch(WASM_URL), {}); + wasm = module.instance.exports; + } catch (error) { + STATUS.innerHTML = `The compiler did not load, so the answers below are missing. (${esc(error)})`; + return; + } + + const encoder = new TextEncoder(); + const decoder = new TextDecoder(); + const bytes = () => new Uint8Array(wasm.memory.buffer); + + const read = () => { + const ptr = wasm.deed_result_ptr(); + const len = wasm.deed_result_len(); + const text = decoder.decode(bytes().slice(ptr, ptr + len)); + wasm.deed_free(ptr, len); + return text; + }; + + wasm.deed_version(); + const reported = read(); + if (reported !== VERSION) { + STATUS.innerHTML = `This page pinned ${esc(VERSION)} and the module says ${esc(reported)}, so it is not being used.`; + return; + } + + const ask = (verb, source) => { + const input = encoder.encode(source); + const ptr = wasm.deed_alloc(input.length); + bytes().set(input, ptr); + wasm[verb](ptr, input.length); + const text = read(); + wasm.deed_free(ptr, input.length); + return text + .split("\n") + .filter((line) => line.trim() !== "") + .map((line) => JSON.parse(line)); + }; + + for (const { id, verb, source } of ASKS) { + const sent = document.getElementById(`${id}-sent`); + const got = document.getElementById(`${id}-got`); + if (!sent || !got) continue; + sent.textContent = source.trimEnd(); + // Indented for reading. On the wire each of these is one line, which is + // the only thing changed about it here. + got.textContent = ask(verb, source) + .map((line) => JSON.stringify(line, null, 2)) + .join("\n\n"); + } + + STATUS.innerHTML = + `Deed ${esc(reported)}, ` + + `${TAG}, ` + + `asked in this tab. Every answer below came back just now.`; +} + +load(); diff --git a/errors/index.html b/errors/index.html index dee429f..91647d7 100644 --- a/errors/index.html +++ b/errors/index.html @@ -49,6 +49,7 @@

A function can only do what its signature admits to.