Skip to content

A page for the argument the language is built on #42

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
onatozmenn merged 1 commit into from
Aug 9, 2026
Merged

A page for the argument the language is built on #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
238 changes: 238 additions & 0 deletions agents/index.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,238 @@
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>For agents | Deed</title>
<meta
name="description"
content="Deed ships a Model Context Protocol server, so the thing writing the code can ask the compiler instead of remembering. It answers with which obligations were proved and which were left to a runtime check."
/>
<link rel="icon" href="../assets/brand/deed-cipher-favicon.ico" sizes="any" />
<link
rel="preload"
as="font"
type="font/woff2"
href="../assets/fonts/ia-writer-mono-latin-400-normal.woff2"
crossorigin
/>
<link
rel="preload"
as="font"
type="font/woff2"
href="../assets/fonts/ia-writer-mono-latin-700-normal.woff2"
crossorigin
/>
<link rel="stylesheet" href="../assets/style.css" />
</head>
<body>
<div class="wrap">
<header class="site">
<div class="header-section">
<div class="header-frame">
<h1>
<a href="../"
><svg class="mark" viewBox="0 0 512 512" aria-hidden="true" focusable="false">
<path d="M176 116H104V396H176" fill="none" stroke="currentColor" stroke-width="56" />
<rect x="236" y="128" width="200" height="56" fill="#24d05a" />
<rect x="236" y="228" width="148" height="56" fill="#eb4888" />
<rect x="236" y="328" width="176" height="56" fill="#10a2f5" />
</svg
>Deed</a
>
</h1>
<h2>A function can only do what its signature admits to.</h2>
</div>
</div>
</header>

<nav class="site">
<a href="../one-clause/">One clause</a>
<a href="../play/">Playground</a>
<a href="./" class="active">For agents</a>
<a href="../errors/">Diagnostics</a>
<a href="../install/">Install</a>
<a href="https://github.com/deed-lang/deed">Source</a>
</nav>

<main>
<h1>For agents</h1>
<p class="lede">
Most code being written now is not typed out by a person. Deed is
built on that being true, and <code>deed mcp</code> 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.
</p>
<p class="status" id="status" aria-live="polite">loading the compiler</p>

<!--
Every transcript on this page is filled in by assets/agents.js from
the pinned artifact, in the reader's tab. Nothing below is a sample
output written here, which is the same rule the playground and the
diagnostics index follow, and it matters more here than anywhere:
this page is a claim about what a machine gets back.
-->

<h2>What comes back that a type error does not</h2>
<p>
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
<em>settled</em>, and which it could only arrange to check at
runtime. That is a gradient, and something iterating on its own
output can climb it.
</p>
<pre class="code"><code id="tiers-sent">…</code></pre>
<pre class="code"><code id="tiers-got">…</code></pre>
<p>
<code>proven</code> means the checker discharged it at compile time.
<code>tested</code> means it produced a property and ran it. Neither
was asked for.
</p>

<h2>And when it cannot</h2>
<p>
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.
</p>
<pre class="code"><code id="guarded-sent">…</code></pre>
<pre class="code"><code id="guarded-got">…</code></pre>
<p>
<em>Nothing narrowed this name</em> 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.
</p>

<h2>A repair, and the reason behind it</h2>
<p>
Models reach for <code>export</code>, because most languages have one.
Across
<a href="https://github.com/deed-lang/deed/blob/main/benchmarks/RESULTS.md"
>five recorded runs</a
>
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:
</p>
<pre class="code"><code id="repair-sent">…</code></pre>
<pre class="code"><code id="repair-got">…</code></pre>
<p>
<code>machine-applicable</code> 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.
</p>

<h2>A test nobody wrote</h2>
<p>
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:
</p>
<pre class="code"><code id="property-sent">…</code></pre>
<pre class="code"><code id="property-got">…</code></pre>
<p>
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.
</p>

<h2>Wiring it up</h2>
<p>
The server speaks MCP on stdin and stdout, so a client starts it the
way it starts any other:
</p>
<pre class="code"><code>{
"mcpServers": {
"deed": { "command": "deed", "args": ["mcp"] }
}
}</code></pre>
<p>
There is nothing else to install; see
<a href="../install/">Install</a>. Six tools:
<code>deed_check</code>, <code>deed_test</code>,
<code>deed_run</code>, <code>deed_fmt</code>, <code>deed_fix</code>
and <code>deed_explain</code>. The full walkthrough is
<a
href="https://github.com/deed-lang/deed/blob/main/how-to/let-an-agent-use-the-compiler.md"
>in the repository</a
>.
</p>

<h2>What it is not allowed to do</h2>
<p>
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.
</p>
<p>
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.
</p>

<h2>Does it actually help?</h2>
<p>
Measured, not asserted. Six tasks, one model, five runs, against a
control arm with the compiler taken away:
</p>
<table class="files">
<thead>
<tr>
<th scope="col">Arm</th>
<th scope="col">Answered</th>
<th scope="col">Check</th>
<th scope="col">Pass their tests</th>
</tr>
</thead>
<tbody>
<tr>
<td>prompt only</td>
<td>6/6</td>
<td>0</td>
<td>0</td>
</tr>
<tr>
<td>with <code>deed mcp</code></td>
<td>6/6</td>
<td>5 or 6</td>
<td>5</td>
</tr>
</tbody>
</table>
<p>
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.
</p>
<p>
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.
<a href="https://github.com/deed-lang/deed/blob/main/benchmarks/RESULTS.md"
>Read it</a
>
before quoting it.
</p>
</main>

<footer class="site">
<p>
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.
</p>
<p>
Apache-2.0. This page has no analytics, no cookies and no third-party
requests.
</p>
</footer>
</div>
<script src="../assets/color.js"></script>
<script src="../assets/agents.js"></script>
</body>
</html>
149 changes: 149 additions & 0 deletions assets/agents.js
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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, "&amp;")
.replace(/</g, "&lt;")
.replace(/>/g, "&gt;");
}

async function load() {
let wasm;
try {
const module = await WebAssembly.instantiateStreaming(fetch(WASM_URL), {});
wasm = module.instance.exports;
} catch (error) {
STATUS.innerHTML = `<span class="d-error">The compiler did not load, so the answers below are missing. (${esc(error)})</span>`;
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 = `<span class="d-error">This page pinned ${esc(VERSION)} and the module says ${esc(reported)}, so it is not being used.</span>`;
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)}, ` +
`<a href="https://github.com/deed-lang/deed/releases/tag/${TAG}">${TAG}</a>, ` +
`asked in this tab. Every answer below came back just now.`;
}

load();
Loading