Commit 6deb96a
authored
docs: ArghDA vision, architecture & roadmap (#1)
## What this is
A planning artefact — `docs/arghda-vision.adoc` — that plans out ArghDA
as the estate's **visual proof-wiring / wiring-diagram tool**,
complementing the existing MVP spec (`docs/arghda-spec.adoc`). No engine
or proof code is touched.
It was synthesised from a read-only survey of `arghda-core`,
`rsr-template-repo`/`standards`, `kategoria`, `ideas-to-alphas`,
`typell`, `nextgen-typing`, `panll`, `affinescript`,
`developer-ecosystem`, `hybrid-automation-router`, `echo-types`,
`absolute-zero`, and `nextgen-language-evangeliser`.
## Key decisions captured
- **Hard boundary:** ArghDA organises / visualises / communicates
proofs; **Agda proves** (directly or via Echidna). It never proves
anything itself.
- **Three-layer architecture:** keep & extend the Rust **`arghda-core`**
engine + a new AffineScript **`arghda-studio`** visual tool (→
typed-wasm / Deno-ESM) + a later **`arghda-panll`** PanLL embedding.
- **Honest AffineScript feasibility position:** the interactive DOM path
is blocked today (#255 loops-don't-run in wasm; #555 effect handlers;
"typed-wasm" is a narrow opt-in verifier). **Resolution:** v1 renders
the DAG as **static SVG/HTML via pure functions**, sidestepping the
broken path; the interactive canvas is deferred, with ArghDA as the
forcing function for the toolchain fixes.
- **The heart:** one richly-tagged **proof-node graph** (status ×
soundness × dependency × glyph × multi-register narrative) — a superset
of the spec's DAG JSON.
- **Feature set** mined from real pain: take-from (import
imports/soundness/ledgers, flag orphans & drift) / visualise
(status-coloured DAG, lattice & matrix views, refuted-route walls) /
put-back (regenerate `All.agda`/`Smoke.agda`, sync labels, emit ledgers
& session-arcs, export CI gates).
- **Communication model** from `nextgen-language-evangeliser`:
RAW/FOLDED/GLYPHED registers, Makaton-style glyphs, a 5-slot no-shame
narrative, audience-parameterised, honest-scope labelling.
- **Integration seams:** Echidna (Zig-API service #3, port 8090) as the
prover backend; TypeLL `ProofObligation`s (:7800); HAR for the "proofs
go programmatic" stage; Groove discovery for PanLL; `kategoria`'s
composition lattice + `ideas-to-alphas`' graduation pipeline as
proof-state sources.
- **RSR-compliant shape** for the proposed `arghda-studio` repo, the
`arghda-core` work needed to finish the spec, a six-phase roadmap, and
an open-decisions/risks register.
## Status
Draft, for review. This is the plan, not the build — it sets up the next
phases (finishing the engine, scaffolding `arghda-studio`).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
---
_Generated by [Claude
Code](https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs)_1 file changed
Lines changed: 766 additions & 0 deletions
0 commit comments