Skip to content

Commit eb28c4d

Browse files
claudehyperpolymath
authored andcommitted
docs(changelog): record kitchenspeak Echo bridge machine-check + PoachedEgg fix
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
1 parent 5f109f5 commit eb28c4d

1 file changed

Lines changed: 19 additions & 0 deletions

File tree

CHANGELOG.md

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,25 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
66

77
All notable changes to the nextgen-languages parent repository.
88

9+
## 2026-06-12
10+
11+
### Changed
12+
13+
- *KitchenSpeak Echo bridge is now MACHINE-CHECKED against the real
14+
`hyperpolymath/echo-types` library.* `kitchenspeak/proofs/agda/EchoBridge.agda`
15+
previously carried a "hand-verified, not machine-checked" caveat; it now
16+
typechecks against the real `Echo` (the `@` sensor witness IS
17+
`Echo (fired sensor thr) true`). The wider echo-types ↔ typesystem
18+
integration is recorded in echo-types'
19+
`docs/bridges/cross-repo-bridge-status.md`.
20+
21+
### Fixed
22+
23+
- `kitchenspeak/proofs/agda/PoachedEgg.agda`: stdlib v2.3 API drift
24+
(`toWitness {Q = …}``{a? = …}`) so the KitchenSpeak proof suite
25+
(Dough + PoachedEgg + EchoBridge) type-checks on the echo-types CI
26+
toolchain (Agda 2.6.3 + stdlib v2.3).
27+
928
## 2026-06-02
1029

1130
### Added

0 commit comments

Comments
 (0)