Skip to content

Point at the page that answers instead of describing - #955

Merged
onatozmenn merged 1 commit into
mainfrom
point-at-the-agents-page
Aug 9, 2026
Merged

Point at the page that answers instead of describing#955
onatozmenn merged 1 commit into
mainfrom
point-at-the-agents-page

Conversation

@onatozmenn

Copy link
Copy Markdown
Collaborator

Stage 1's second item: https://deed-lang.github.io/agents/ (site
deed-lang/deed-lang.github.io#42).

deed mcp had one paragraph, on the install page. That is not where somebody
deciding whether to wire a compiler into an agent is reading.

The page does not describe what comes back, it shows it. Every transcript on it
is filled in by the pinned compiler running in the reader's tab, for the program
printed above it, so it cannot claim an answer this compiler does not give:

  • an obligation line carrying a tier, proven and tested in the same answer;
  • the same refinement without its precondition, coming back guarded with
    "reason": "nothing narrowed this name";
  • the export diagnostic with its machine-applicable edit and the note saying
    why the word does not exist;
  • deed_test running a property generated from a contract, in a module with no
    tests in it.

The benchmark from #954 is there as a table with the control arm beside it and a
link to benchmarks/RESULTS.md, with the three things it does not establish
stated rather than dropped.

This PR is the two lines in this repository that follow from that: the roadmap
item, and a pointer from how-to/let-an-agent-use-the-compiler.md, because
seeing the answers is cheaper than configuring a server to find out what they
look like.

Stage 1's second item is done: <https://deed-lang.github.io/agents/>. It had
been one paragraph on the install page, which is not where somebody deciding
whether to wire a compiler into an agent is reading.

The page fills every transcript in from the pinned compiler in the reader's
tab, so it cannot claim an answer this compiler does not give: an obligation
line carrying a tier, a `guarded` one with its reason, the `export` repair with
its note, and a property generated from a contract in a module with no tests.

The how-to now points at it, because seeing the answers is cheaper than
configuring a server to find out what they look like.
@onatozmenn
onatozmenn merged commit 55c83dc into main Aug 9, 2026
10 checks passed
@onatozmenn
onatozmenn deleted the point-at-the-agents-page branch August 9, 2026 11:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant