From 10f33a7d9c336646f4b646758670e1566b36e025 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 12 Jun 2026 22:57:38 +0000 Subject: [PATCH] docs(changelog): record kitchenspeak Echo bridge machine-check + PoachedEgg fix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 2026-06-12 entry: EchoBridge.agda upgraded hand-verified → machine-checked vs the real echo-types Echo; PoachedEgg.agda stdlib v2.3 toWitness drift fixed. Cross-repo integration ledger lives in echo-types docs/bridges/cross-repo-bridge-status.md. https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS --- CHANGELOG.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e281dc1..aac2072 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,25 @@ Copyright (c) Jonathan D.A. Jewell All notable changes to the nextgen-languages parent repository. +## 2026-06-12 + +### Changed + +- *KitchenSpeak Echo bridge is now MACHINE-CHECKED against the real + `hyperpolymath/echo-types` library.* `kitchenspeak/proofs/agda/EchoBridge.agda` + previously carried a "hand-verified, not machine-checked" caveat; it now + typechecks against the real `Echo` (the `@` sensor witness IS + `Echo (fired sensor thr) true`). The wider echo-types ↔ typesystem + integration is recorded in echo-types' + `docs/bridges/cross-repo-bridge-status.md`. + +### Fixed + +- `kitchenspeak/proofs/agda/PoachedEgg.agda`: stdlib v2.3 API drift + (`toWitness {Q = …}` → `{a? = …}`) so the KitchenSpeak proof suite + (Dough + PoachedEgg + EchoBridge) type-checks on the echo-types CI + toolchain (Agda 2.6.3 + stdlib v2.3). + ## 2026-06-02 ### Added