From 62e2a611b3b9a3d822f9d194c2d434ab6077663b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 30 Apr 2026 18:15:54 +0100 Subject: [PATCH] chore(policy): recognise Agda + echo-types as canonical loss-with-residue formalism Adds Agda to Tier-1 alongside the existing Tier-1 set in three RSR_OUTLINE.adoc copies (with the ReScript -> AffineScript and Rust -> Rust(+SPARK) updates from PR #35 inlined to avoid build conflict). Adds two new rows to .claude/CLAUDE.md: - Agda (formal verification, foundational/type-theoretic) - echo-types library (canonical loss-with-residue formalism; cite from hyperpolymath/echo-types rather than reinventing) Reframes Idris2 row from 'sole option' to 'primary, ABI-style proofs' since Agda now formally complements it. Updates ai-instruction/sonnet.md hard-rules language-policy line to list AffineScript first, include Agda explicitly, ban ReScript, and reference RS/TS/JS -> AffineScript -> typed-wasm. Coordinates with: hyperpolymath/echo-types#29 (.scm -> .a2ml + Justfile fix) hyperpolymath/echo-types#30 (RSR floor scaffolding) hyperpolymath/standards#33 (REQUIRED-FILES doc-drift fix) hyperpolymath/standards#35 (ReScript -> AffineScript sweep; line-overlap with this PR; mechanical rebase at merge) Co-Authored-By: Claude Opus 4.7 (1M context) --- .claude/CLAUDE.md | 4 +++- 0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc | 2 +- 0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc | 2 +- ai-instruction/sonnet.md | 4 ++-- consent-aware-http/RSR_OUTLINE.adoc | 2 +- 5 files changed, 8 insertions(+), 6 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 0d197895..e3025dd5 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -36,7 +36,9 @@ for the canonical statement. | **Deno** | Runtime & package management | Replaces Node/npm/bun | | **Rust/SPARK** | Performance-critical, systems, WASM, CLI tools, safety-critical | "Rust" always means "Rust/SPARK" per terminology note above. Preferred over Ada where reachable. | | **Zig** | FFI layer (hyperpolymath ABI/FFI standard), memory-safe systems where Rust/SPARK is overkill | Also the migration target for V-lang | -| **Idris2** | Formal verification (sole option) | ATS2 rejected. Proven-library status in `proven` repo. | +| **Idris2** | Formal verification (primary, ABI-style proofs) | ATS2 rejected. Proven-library status in `proven` repo. | +| **Agda** | Formal verification (foundational / type-theoretic constructions) | Used by `hyperpolymath/echo-types` (loss-with-residue / proof-relevant fibers) and other foundational formalisations. Constructive only — no postulates in load-bearing tracks. | +| **echo-types library** | Loss-with-residue formalism (Agda) | `hyperpolymath/echo-types` — canonical formalisation of `Echo f y := Σ (x : A) , (f x ≡ y)`. Cite from this lib rather than reinventing in downstream code. | | **Tauri 2.0+** | Mobile apps (iOS/Android) | Rust backend + web UI | | **Dioxus** | Mobile apps (native UI) | Pure Rust, React-like | | **Gleam** | Backend services | Runs on BEAM or compiles to JS | diff --git a/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc b/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc index 705d6dc1..d1be7bd6 100644 --- a/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc +++ b/0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc @@ -146,7 +146,7 @@ project/ === Language Tiers -* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript +* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix * **Infrastructure**: Guix channels, derivations diff --git a/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc b/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc index 705d6dc1..d1be7bd6 100644 --- a/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc +++ b/0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc @@ -146,7 +146,7 @@ project/ === Language Tiers -* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript +* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix * **Infrastructure**: Guix channels, derivations diff --git a/ai-instruction/sonnet.md b/ai-instruction/sonnet.md index 87077343..5df38d9a 100644 --- a/ai-instruction/sonnet.md +++ b/ai-instruction/sonnet.md @@ -83,8 +83,8 @@ You are implementing in . - -- +- - -