Skip to content

Commit 5c1e309

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs+config: wrap-up — 6a2 refresh, Hypatia waiver registry, contractiles, branch hygiene (#67)
Documentation + configuration wrap-up for the KitchenSpeak / echo-types / CI-hygiene work, and the change that makes recurring CI advisories **self-handling**. Intended to **merge to main** once CI is green (per maintainer authorization). ## Documentation (highest-standards refresh) - **README.adoc** — new "Shared Formal Substrate — echo-types" section. - **EXPLAINME.adoc** — echo-types/ADR-0004 note on KitchenSpeak + new "Governance & CI Posture" section. - **6a2**: `STATE` (kitchenspeak + ci-governance), `META` (ADRs, practices, external rulesets), `ECOSYSTEM` (echo-types, EchoTypes.jl, standards, typed-wasm). `CHANGELOG.md` + `TOOLING-STATUS.adoc` refreshed. ## Hypatia / gitbot self-handling The enforcing ruleset lives in `hyperpolymath/standards` (out of scope), so the in-repo lever is a **machine-readable waiver registry**: - **`6a2/NEUROSYM.a2ml` `[waivers]`** — every recurring advisory triaged once: reusable-caller `timeout` false-positives, `governance@main` pin (track), scorecard/instant-sync detector mismatches (addressed), by-design `agda_postulate` axioms. - **`6a2/PLAYBOOK.a2ml`** — gitbot runbook (consult the registry, skip accepted findings, don't re-fix) + branch-hygiene + merge-gating. - **`6a2/AGENTIC.a2ml`** — agent CI-handling + branch-hygiene contract. ## Contractiles - **`MUST.contractile`** — project-specific invariants (proofs-first, trusted-base documentation, echo-types attachment, waiver discipline). - **`Trustfile`** — branch-hygiene reconciliation: deleting **merged** PR branches is now permitted; force-push / CI-secret modification / publish remain denied. ## Also done outside this PR - The four merged feature branches (#63–#66) were deleted (they were already auto-removed on merge; local refs pruned). ## Validation - All six `6a2/*.a2ml` parse as valid TOML; `MUST.contractile` s-expr paren-balanced; SPDX headers intact on all changed files (README has none on `main` either — docs exempt). ## Honest limitation Hypatia's enforcing ruleset is external; this PR records the accepted findings repo-side so agents stop re-litigating them, but **full auto-suppression of the addressed/false-positive items needs a one-time `standards`-side change** — tracked in each waiver's `action`. https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY --- _Generated by [Claude Code](https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 30d7f50 commit 5c1e309

12 files changed

Lines changed: 260 additions & 17 deletions

File tree

‎.machine_readable/6a2/AGENTIC.a2ml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,3 +22,13 @@ can-create-files = true
2222
# - Never use banned languages (TypeScript, Python, Go, etc.)
2323
# - Never place state files in repository root (must be in .machine_readable/)
2424
# - Never use AGPL license (use MPL-2.0)
25+
26+
[agent-ci-handling]
27+
# How agents/gitbots should treat CI on this repo.
28+
hypatia-advisory = "non-blocking; consult .machine_readable/6a2/NEUROSYM.a2ml [waivers] before acting on any finding"
29+
do-not-refix = "findings recorded as accepted/by-design/false-positive in the waiver registry must not be re-fixed"
30+
runbook = "see .machine_readable/6a2/PLAYBOOK.a2ml [recurring-ci-advisories]"
31+
32+
[agent-branch-hygiene]
33+
delete-merged-branches = "allowed (merged PR branches only) per Trustfile carve-out"
34+
never = "delete main/active branches; force-push; modify CI secrets; publish"

‎.machine_readable/6a2/ECOSYSTEM.a2ml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,15 @@ ecosystem = "hyperpolymath"
88

99
[position]
1010
type = "component"
11+
12+
[related-projects]
13+
# Projects this repo coordinates with directly.
14+
echo-types = "hyperpolymath/echo-types — Agda formal model of structured loss (Echo fiber); KitchenSpeak's Echo substrate"
15+
echotypes-jl = "hyperpolymath/EchoTypes.jl — executable finite-domain companion to echo-types (runtime model, not a proof)"
16+
standards = "hyperpolymath/standards — governance + Hypatia reusable workflows (pinned)"
17+
typed-wasm = "hyperpolymath/typed-wasm — WasmGC compilation target for AffineScript/Ephapax"
18+
tentacles = "hyperpolymath/tentacles-agentic-syllabus — curriculum (NOT a language; do not audit as one)"
19+
20+
[language-repos]
21+
note = "Each language is a standalone canonical repo, wired in as a submodule (see .gitmodules)."
22+
kitchenspeak = "in-tree, standalone-repo-ready; elevate via scripts/elevate-kitchenspeak.sh"

‎.machine_readable/6a2/META.a2ml‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,23 @@ project = "nextgen-languages"
77
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
88
license = "MPL-2.0"
99
standard = "RSR 2026"
10+
11+
[architecture-decisions]
12+
# Repo-level and per-language ADRs (kitchenspeak ADRs under kitchenspeak/decisions/).
13+
ks-0001 = "Proof assistant for KitchenSpeak: Agda (Lean 4 reserved as successor)"
14+
ks-0002 = "Elevate KitchenSpeak to a standalone repository + submodule"
15+
ks-0003 = "Base KitchenSpeak's Echo type on the hyperpolymath/echo-types library"
16+
ks-0004 = "Echo attaches to Linear/Dyadic consumption (B-now / C-later / A-shim)"
17+
18+
[practices]
19+
proofs-first = "KitchenSpeak leads with Agda proofs (its Agda-Proven invariant) ahead of compiler work"
20+
ci-hygiene = "All real jobs carry timeout-minutes; actions SHA-pinned; reusable-caller jobs exempt from timeout"
21+
hypatia-waivers = "Recurring scan advisories are triaged once in NEUROSYM.a2ml [waivers], not re-fixed per PR"
22+
adr-granularity = "Architecture-decision PRs are kept separate from implementation PRs"
23+
checkpoints = "Coherent, reversible work is checkpointed via draft PRs to survive ephemeral environments"
24+
25+
[external-rulesets]
26+
# Governance/scan logic lives in the standards repo, consumed via pinned reusables.
27+
governance = "hyperpolymath/standards governance-reusable.yml"
28+
hypatia = "hyperpolymath/standards hypatia-scan-reusable.yml"
29+
note = "Changes to the enforcing rulesets must be made in standards, not here."

‎.machine_readable/6a2/NEUROSYM.a2ml‎

Lines changed: 72 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,14 @@
22
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
#
44
# NEUROSYM.a2ml — Neurosymbolic integration metadata
5-
# Configuration for Hypatia scanning and symbolic reasoning.
5+
# Configuration for Hypatia scanning and symbolic reasoning, plus the
6+
# repo-local registry of accepted/triaged Hypatia findings (waivers) that
7+
# Hypatia and the gitbots consult so the same advisories are not
8+
# re-litigated on every PR.
69

710
[metadata]
8-
version = "0.1.0"
9-
last-updated = "2026-03-16"
11+
version = "0.2.0"
12+
last-updated = "2026-06-02"
1013

1114
[hypatia-config]
1215
scan-enabled = true
@@ -24,3 +27,69 @@ report-format = "logtalk"
2427
# - Output guaranteed to satisfy constraints by construction
2528
# - Value constraints in types
2629
# - SMT solver backed
30+
31+
# ---------------------------------------------------------------------------
32+
# Accepted-findings registry (waivers).
33+
#
34+
# Hypatia's enforcing ruleset lives in hyperpolymath/standards
35+
# (hypatia-scan-reusable.yml / governance-reusable.yml), NOT in this repo,
36+
# so this registry is the repo-local source of truth for findings that have
37+
# been triaged and accepted. The Hypatia scan is advisory (non-blocking);
38+
# the governance gates are the blocking checks and already pass.
39+
#
40+
# Gitbot / agent contract (see AGENTIC.a2ml, PLAYBOOK.a2ml):
41+
# - Before acting on a Hypatia advisory finding, look it up here by `rule`
42+
# + `file`. If present, DO NOT attempt a fix — the finding is accepted.
43+
# - Only act on findings NOT listed here, or whose `disposition` is
44+
# "track" with an open `action`.
45+
#
46+
# disposition values:
47+
# false-positive — the rule does not apply (acting on it would break CI)
48+
# by-design — intentional, documented; not a defect
49+
# addressed — fixed in-repo; detector still fires (pattern mismatch)
50+
# track — accepted for now; carries a follow-up `action`
51+
# ---------------------------------------------------------------------------
52+
53+
[accepted-findings]
54+
policy = "Findings listed below are triaged and accepted; do not auto-fix."
55+
ruleset-location = "hyperpolymath/standards (external to this repo)"
56+
scan-is-blocking = false
57+
58+
[waivers.reusable-caller-timeout]
59+
rule = "missing_timeout_minutes"
60+
files = "governance.yml, hypatia-scan.yml, mirror.yml, scorecard.yml, secret-scanner.yml"
61+
severity = "medium"
62+
disposition = "false-positive"
63+
justification = "These jobs call reusable workflows (jobs.<id>.uses). GitHub Actions rejects timeout-minutes on reusable-workflow caller jobs, so adding it would break the workflow."
64+
65+
[waivers.governance-reusable-pin]
66+
rule = "unpinned_action"
67+
files = "governance.yml"
68+
severity = "medium"
69+
disposition = "track"
70+
justification = "hyperpolymath/standards governance-reusable.yml is referenced at @main. The standards repo is outside this session's scope and the SHA could not be resolved here; the check is green at @main."
71+
action = "Pin to a commit SHA via an authenticated lookup of standards governance-reusable.yml on main."
72+
73+
[waivers.scorecard-publish-split]
74+
rule = "scorecard_publish_with_run_step"
75+
files = "scorecard-enforcer.yml"
76+
severity = "high"
77+
disposition = "addressed"
78+
justification = "The privileged publish job (id-token: write) was split from a separate unprivileged score-gate job; the publish job has no run steps. Detector may want the publish in a separate workflow file rather than a separate job in the same file."
79+
action = "If suppression is required, confirm the detector's exact shape with standards, or move the publish step to its own workflow file."
80+
81+
[waivers.instant-sync-secret-gate]
82+
rule = "secret_action_without_presence_gate"
83+
files = "instant-sync.yml"
84+
severity = "high"
85+
disposition = "addressed"
86+
justification = "The repository-dispatch step is gated on FARM_DISPATCH_TOKEN presence via a job-level env plus a step-level `if`. Detector may expect a job-level gate."
87+
action = "If suppression is required, confirm the detector's expected gate shape with standards."
88+
89+
[waivers.agda-postulate-trusted-base]
90+
rule = "agda_postulate"
91+
files = "kitchenspeak/proofs/agda/Dough.agda, kitchenspeak/proofs/agda/PoachedEgg.agda"
92+
severity = "critical"
93+
disposition = "by-design"
94+
justification = "These postulates are KitchenSpeak's deliberate trusted base: postulated echo-oracle sensor streams and the GENTLE controller spec. Each is annotated inline (AXIOM:) and enumerated in PROOF-NEEDS.md; they are documented trust boundaries, not undocumented soundness holes. The blocking Trusted-base reduction policy passes."
95+
action = "Replaced by verified HAL bindings in a production lowering; tracked in PROOF-NEEDS.md."

‎.machine_readable/6a2/PLAYBOOK.a2ml‎

Lines changed: 37 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,18 +2,19 @@
22
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
#
44
# PLAYBOOK.a2ml — Operational playbook
5-
# Runbooks, incident response, deployment procedures.
5+
# Runbooks, incident response, deployment procedures, and the standing
6+
# operating contract for automated agents (gitbots) on this repo.
67

78
[metadata]
8-
version = "0.1.0"
9-
last-updated = "2026-03-16"
9+
version = "0.2.0"
10+
last-updated = "2026-06-02"
1011

1112
[deployment]
1213
# method = "gitops"
1314
# target = "container"
1415

1516
[incident-response]
16-
# 1. Check .machine_readable/STATE.a2ml for current status
17+
# 1. Check .machine_readable/6a2/STATE.a2ml for current status
1718
# 2. Review recent commits and CI results
1819
# 3. Run just validate to check compliance
1920

@@ -24,3 +25,35 @@ last-updated = "2026-03-16"
2425

2526
[operational-flows]
2627
# - Adding a new language to the ecosystem
28+
29+
# ---------------------------------------------------------------------------
30+
# Recurring CI advisories — gitbot runbook.
31+
#
32+
# The Hypatia neurosymbolic scan posts an advisory comment on every PR. It
33+
# is NON-BLOCKING; the blocking gates are the governance/* and scan/* checks.
34+
# Most advisory findings are already triaged and recorded in
35+
# .machine_readable/6a2/NEUROSYM.a2ml [waivers].
36+
# ---------------------------------------------------------------------------
37+
38+
[recurring-ci-advisories]
39+
source = "Hypatia Security Scan advisory comment"
40+
blocking = false
41+
registry = ".machine_readable/6a2/NEUROSYM.a2ml"
42+
step-1 = "For each finding, look it up in NEUROSYM [waivers] by rule + file."
43+
step-2 = "If present, skip it — it is accepted; do NOT open a fix."
44+
step-3 = "Act only on findings NOT in the registry, or with disposition = track and an open action."
45+
step-4 = "If a genuinely new finding appears, triage it; if accepted, add a waiver entry rather than re-fixing each PR."
46+
47+
[branch-hygiene]
48+
# Permitted per the Trustfile carve-out (contractiles/trust/Trustfile.a2ml).
49+
delete-merged-branches = "allowed — feature branches whose PR is merged may be deleted (local + remote)"
50+
never-delete = "main, and any open/active branch"
51+
never = "force-push; modify CI secrets; publish"
52+
note = "GitHub auto-deletes PR branches on merge; prune local tracking refs with `git remote prune origin`."
53+
54+
[merge-gating]
55+
# When self-merging (per maintainer authorization), gate on:
56+
rule-1 = "All required (blocking) checks green: governance/*, scan/*, analyze, semgrep, dogfood, validators."
57+
rule-2 = "Hypatia advisory is non-blocking and MUST NOT gate the merge."
58+
rule-3 = "Draft/WIP PRs are never merged; mark ready first."
59+
rule-4 = "Architecture-decision PRs (ADRs) and implementation PRs are kept at separate granularity."

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@
55
[metadata]
66
project = "nextgen-languages"
77
version = "0.1.0"
8-
last-updated = "2026-04-04"
8+
last-updated = "2026-06-02"
99
status = "active"
1010

1111
[project-context]
1212
name = "nextgen-languages"
1313
completion-percentage = 15
14-
phase = "CRG C achieved for ephapax workspace (2026-04-04)"
14+
phase = "CRG C achieved for ephapax workspace (2026-04-04); KitchenSpeak elevated + proofs commenced (2026-06)"
1515

1616
[crg-status]
1717
overall = "CRG C achieved 2026-04-04"
@@ -31,3 +31,23 @@ ephapax-lexer-new = "9 new tests: 4 P2P property, 2 E2E, 3 aspect"
3131
p2p-property-tests = "Loop-based invariant checks (10-20 iterations each)"
3232
e2e-tests = "Full pipeline: lexer->tokens, module->discipline check"
3333
aspect-tests = "Robustness: empty inputs, stateless checkers, edge cases"
34+
35+
[kitchenspeak]
36+
# KitchenSpeak: experimental, formally-verified kitchen-orchestration DSL.
37+
status = "elevated to standalone-repo-ready; proofs-first development commenced"
38+
listed-as = "DSL in README.adoc and EXPLAINME.adoc"
39+
elevation = "scripts/elevate-kitchenspeak.sh creates hyperpolymath/kitchenspeak + submodule (needs repo-create rights)"
40+
proofs = "Dough.agda, PoachedEgg.agda (Linear+Tropical+Echo), EchoBridge.agda; harness: proofs/Makefile + kitchenspeak.agda-lib"
41+
proofs-status = "hand-verified, not yet machine-checked (Agda not in CI yet; ROADMAP Phase 1a)"
42+
decisions = "ADR 0001 (Agda), 0002 (elevation), 0003 (echo-types dependency), 0004 (Echo attaches to Linear/Dyadic: B-now/C-later/A-shim)"
43+
echo-types = "Echo type bound to hyperpolymath/echo-types fiber; canonical attachment is Linear/Dyadic per ADR 0004; Bool bridge is a temporary smoke-test"
44+
gated = "B-implementation gated on echo-types repo in scope (read EchoLinear/EchoTropical/EchoChoreo/EchoEpistemic/EchoResidueTaxonomy first)"
45+
46+
[ci-governance]
47+
# Outcome of the 2026-06 CI hygiene pass.
48+
timeouts = "timeout-minutes added to all real runs-on+steps jobs (reusable-caller jobs intentionally excluded)"
49+
codeql = "matrix switched javascript-typescript -> actions (repo has no JS/TS sources)"
50+
nuget = "spurious nuget dependabot ecosystem removed (no .NET projects)"
51+
scorecard = "publish job split from unprivileged score-gate job"
52+
instant-sync = "repository-dispatch gated on FARM_DISPATCH_TOKEN presence"
53+
hypatia-waivers = "recurring advisory findings triaged in .machine_readable/6a2/NEUROSYM.a2ml [waivers]"

‎.machine_readable/MUST.contractile‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -78,11 +78,16 @@
7878
; ABI/FFI (if applicable)
7979
(must "no modification of ABI contracts without proof update")
8080
(must "no removal of formal verification proofs")
81-
)
8281

83-
; === Project-Specific Invariants ===
84-
; *REMINDER: Add invariants specific to this repo*
85-
; (must "# Add project-specific invariants here")
82+
; === Project-Specific Invariants (nextgen-languages) ===
83+
; Proofs and trusted base
84+
(must "KitchenSpeak Agda postulates are documented as trusted base (inline AXIOM + PROOF-NEEDS.md)")
85+
(must "KitchenSpeak proofs lead implementation — the Agda-Proven invariant")
86+
(must "KitchenSpeak Echo type attaches to Linear/Dyadic per ADR 0004; the Bool bridge is non-canonical")
87+
; Governance and cross-repo rulesets
88+
(must "recurring Hypatia advisories are triaged in NEUROSYM.a2ml waivers, not silently suppressed")
89+
(must "echo-types and Hypatia rulesets are changed in their source repos, not vendored here")
90+
)
8691

8792
(enforcement
8893
(k9-validator "contractiles/k9/must-check.k9.ncl")

‎CHANGELOG.md‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,38 @@
33

44
All notable changes to the nextgen-languages parent repository.
55

6+
## 2026-06-02
7+
8+
### Added
9+
10+
- KitchenSpeak elevated to standalone-repo-ready and listed as a DSL in
11+
`README.adoc` / `EXPLAINME.adoc`; `scripts/elevate-kitchenspeak.sh` performs
12+
the repo split + submodule conversion.
13+
- KitchenSpeak proofs commenced: `PoachedEgg.agda` (Linear+Tropical+Echo),
14+
`EchoBridge.agda`, and a proof harness (`proofs/Makefile`,
15+
`kitchenspeak.agda-lib`).
16+
- KitchenSpeak ADRs 0002–0004: standalone elevation; `echo-types` dependency;
17+
Echo attaches to Linear/Dyadic (B-now / C-later / A-shim).
18+
- Hypatia accepted-findings registry in `.machine_readable/6a2/NEUROSYM.a2ml`
19+
`[waivers]`, with gitbot runbook in `PLAYBOOK.a2ml` and agent contract in
20+
`AGENTIC.a2ml`.
21+
- `6a2` machine-readable state refreshed (STATE/META/ECOSYSTEM/NEUROSYM/
22+
PLAYBOOK/AGENTIC); `MUST.contractile` project-specific invariants.
23+
24+
### Changed
25+
26+
- CI hygiene: `timeout-minutes` on all real jobs; CodeQL matrix
27+
`javascript-typescript` → `actions`; scorecard publish job split from an
28+
unprivileged score-gate; `instant-sync` dispatch gated on secret presence;
29+
fixed pre-existing invalid YAML in `instant-sync.yml`.
30+
- `Trustfile` reconciled: deleting merged PR branches is permitted
31+
(force-push, CI-secret modification, and publish remain denied).
32+
33+
### Removed
34+
35+
- Spurious `nuget` ecosystem from `.github/dependabot.yml` (no .NET projects).
36+
- Stale merged feature branches.
37+
638
## 2026-03-15
739

840
### Changed

‎EXPLAINME.adoc‎

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,11 @@ Ceremonial (effect), Primitive (units). `max_duration` / `on_fail` /
9999
NOTE: *KitchenSpeak* is an experimental teaching DSL, not one of the ten
100100
core languages. It is maintained as the standalone `hyperpolymath/kitchenspeak`
101101
repository and develops proofs-first (see its `ROADMAP.adoc`); the canonical
102-
recipes (Dough, Poached Egg) already have Agda lowerings.
102+
recipes (Dough, Poached Egg) already have Agda lowerings. Per ADR 0004 its
103+
Echo type is being anchored on the link:https://github.com/hyperpolymath/echo-types[`echo-types`]
104+
library (structured-loss residue), attaching to the *Linear/Dyadic* consumption
105+
types rather than the narrow `@` sensor witness — the current Boolean
106+
`EchoBridge` is a temporary smoke-test, not the canonical attachment.
103107

104108
=== Most mature: Ephapax
105109

@@ -332,6 +336,24 @@ what does not" document.
332336
| Visual map of all language satellites and their relationships.
333337
|===
334338

339+
== Governance & CI Posture
340+
341+
CI governance (the `governance/*` jobs) and the Hypatia neurosymbolic scan are
342+
consumed from `hyperpolymath/standards` as *pinned reusable workflows* — the
343+
enforcing rulesets live there, not in this repo. Two consequences for readers
344+
and for automated agents:
345+
346+
* The *Hypatia Security Scan* comment on PRs is *advisory and non-blocking*.
347+
The blocking gates are the `governance/*`, `scan/*`, `analyze`, `semgrep`,
348+
validator, and dogfood checks.
349+
* Recurring advisory findings that have been triaged and accepted (reusable-
350+
workflow-caller timeout false positives, by-design Agda trusted-base
351+
postulates, etc.) are recorded once in
352+
`.machine_readable/6a2/NEUROSYM.a2ml` under `[waivers]`. Agents consult that
353+
registry (per `AGENTIC.a2ml` / `PLAYBOOK.a2ml`) and do not re-fix accepted
354+
findings on every PR. Changing the enforcing ruleset itself must be done in
355+
`standards`.
356+
335357
== Questions?
336358

337359
Start with `TOOLING-STATUS.adoc` for the current state of each language.

‎README.adoc‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -151,6 +151,23 @@ See also:
151151
* `nextgen-languages/affinescript/` — affine type discipline, compiles to WasmGC
152152
* `nextgen-languages/ephapax/` — dyadic linear/affine type system, compiles to WasmGC
153153

154+
== Shared Formal Substrate — echo-types
155+
156+
Several languages here reason about *irreversible transformation with retained
157+
residue* — an egg cannot be uncracked, flour and water become dough. The
158+
formal account of that idea lives in a separate repository:
159+
160+
* link:https://github.com/hyperpolymath/echo-types[`echo-types`] — a
161+
constructive Agda library for *Echo types*: the proof-relevant residue of
162+
structured (non-total) loss, `Echo f y := Σ (x : A), f x ≡ y`. Its
163+
link:https://github.com/hyperpolymath/EchoTypes.jl[`EchoTypes.jl`] companion
164+
is an executable finite-domain model.
165+
166+
KitchenSpeak is the first consumer: per ADR 0004 its Echo type attaches to the
167+
*Linear/Dyadic* consumption types (where irreversible transformation and
168+
provenance live), with `echo-types` as the substrate. `echo-types` is not a
169+
language in the `nextgen-languages` sense — it is a shared formal library.
170+
154171
== Status
155172

156173
This repository should be read as a *research exploration* rather than a production system.

0 commit comments

Comments
 (0)