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. +

+
+ + +
+ + + + 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.