Skip to content

chore(policy): recognise Agda + echo-types as canonical loss-with-residue formalism #36

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
hyperpolymath merged 2 commits into from
May 1, 2026
+8 −6
Merged

chore(policy): recognise Agda + echo-types as canonical loss-with-residue formalism #36

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
62e2a61
chore(policy): recognise Agda + echo-types as canonical loss-with-res…
hyperpolymath Apr 30, 2026
c276169
Merge branch 'main' into chore/recognise-agda-and-echo-types
hyperpolymath May 1, 2026
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
4 changes: 3 additions & 1 deletion .claude/CLAUDE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down
2 changes: 1 addition & 1 deletion 0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion 0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions ai-instruction/sonnet.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,8 +83,8 @@ You are implementing <one-line task statement> in <repo path>.

- <License headers: SPDX-License-Identifier: PMPL-1.0-or-later unless otherwise
stated (AGPL-3.0-or-later for IDApTIK / Airborne Submarine Squadron)>
- <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Gleam; no
TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm)>
- <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Agda / Gleam; no
TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm; Agda for foundational proofs incl. echo-types)>
- <Testing: run tests before claiming completion; "dune build passes" is NOT
the same as "behaviourally correct" — cite a behavioural check>
- <No dangerous patterns: believe_me, assert_total, Admitted, sorry,
Expand Down
2 changes: 1 addition & 1 deletion consent-aware-http/RSR_OUTLINE.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading