Skip to content

docs: ArghDA vision, architecture & roadmap#1

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/modest-hawking-3fd6it
Jun 18, 2026
Merged

docs: ArghDA vision, architecture & roadmap#1
hyperpolymath merged 1 commit into
mainfrom
claude/modest-hawking-3fd6it

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

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 feat(lint): escape-hatch + tab-mix rules #3, port 8090) as the prover backend; TypeLL ProofObligations (: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.ai/code/session_019GiSiEfgZCte35dyykgBHs


Generated by Claude Code

Adds docs/arghda-vision.adoc — the wider plan for ArghDA as the
estate's visual proof-wiring / wiring-diagram tool, complementing the
existing MVP spec (arghda-spec.adoc).

Covers:
- The hard boundary: ArghDA organises/visualises/communicates proofs;
  Agda proves (directly or via Echidna). It never proves anything.
- The motivating pain mined from echo-types and absolute-zero
  (orphan modules, hidden postulates, invisible dependency order,
  drifting status tables, refuted-route re-walks, merge drift).
- Three-layer architecture: Rust arghda-core (engine) + AffineScript
  arghda-studio (the visual tool, → typed-wasm/Deno-ESM) + arghda-panll
  (PanLL embedding), with a decision record.
- The honest AffineScript feasibility position and the static-SVG/HTML
  resolution for v1 (pure renderers sidestep the broken interactive
  path; interactive canvas deferred with ArghDA as the forcing function).
- The single richly-tagged proof-node graph data model (status x
  soundness x dependency x glyph x multi-register narrative).
- The full feature set: take-from / visualise / put-back.
- The communication model adapted from nextgen-language-evangeliser
  (RAW/FOLDED/GLYPHED registers, Makaton-style glyphs, 5-slot no-shame
  narrative, audience-parameterised, honest-scope labelling).
- Integration seams: Echidna (Zig API service #3), TypeLL obligations,
  HAR programmatic stage, Groove discovery, kategoria + ideas-to-alphas.
- RSR-compliant shape for the proposed arghda-studio repo and the
  arghda-core work needed to finish the spec.
- A six-phase roadmap and an open-decisions/risks register.

Planning artefact only; no engine or proof code changed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
@hyperpolymath
hyperpolymath marked this pull request as ready for review June 18, 2026 11:50
@hyperpolymath
hyperpolymath merged commit 6deb96a into main Jun 18, 2026
1 check passed
@hyperpolymath
hyperpolymath deleted the claude/modest-hawking-3fd6it branch June 18, 2026 11:50
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.

2 participants