diff --git a/.machine_readable/LANGUAGES.a2ml b/.machine_readable/LANGUAGES.a2ml index 329c7ac..7c321aa 100644 --- a/.machine_readable/LANGUAGES.a2ml +++ b/.machine_readable/LANGUAGES.a2ml @@ -4,8 +4,8 @@ # LANGUAGES.a2ml — Migrated from LANGUAGES.scm [metadata] -version = "0.1.0" -last-updated = "2026-03-16" +version = "0.1.1" +last-updated = "2026-06-02" migrated-from = "LANGUAGES.scm" [content] @@ -383,3 +383,26 @@ migrated-from = "LANGUAGES.scm" # - ))) # - The eight languages span a complete spectrum: # - ))) + +# ============================================================================= +# Structured language registry — supersedes the commented s-expression content +# above (legacy, retained for historical reference; do not parse). +# Add new entries here as [languages.]. +# ============================================================================= + +[languages.kitchenspeak] +name = "KitchenSpeak" +kind = "Orchestration DSL" +status = "proofs-first" +phase = "Phase 1 (Dough + PoachedEgg proofs; EchoBridge smoke-test)" +location = "kitchenspeak/" +standalone-repo = "hyperpolymath/kitchenspeak" +standalone-repo-status = "pending — run scripts/elevate-kitchenspeak.sh" +proof-assistant = "Agda 2.6.4+" +stdlib-min = "standard-library 2.3+" +extra-deps = ["echo-types", "absolute-zero"] +types = ["Tropical", "Linear", "Choreographic", "Echo", "Dyadic", "Ceremonial", "Primitive"] +invariant = "Agda-Proven — proofs lead implementation" +adrs = ["0001-proof-assistant", "0002-elevation", "0003-echo-types-dep", "0004-echo-attaches-to-linear-dyadic"] +echo-attachment = "B-now (Linear/Dyadic consumption); C-later (full Echo fiber); A-shim (Bool bridge, non-canonical)" +added = "2026-06-02" diff --git a/contractiles/intend/Intentfile.a2ml b/contractiles/intend/Intentfile.a2ml index 02d1cb7..e8746cc 100644 --- a/contractiles/intend/Intentfile.a2ml +++ b/contractiles/intend/Intentfile.a2ml @@ -10,6 +10,23 @@ Declared intent and purpose for Nextgen Languages. Nextgen Languages — *Parent repository for tracking and coordinating experimental language development* +Current language family: + +| Language / DSL | Kind | Proof status | +|---|---|---| +| AffineScript (Solo / Duet / Ensemble) | General-purpose, affine-typed | Concept v0.1 | +| KitchenSpeak | Orchestration DSL, 7 types, Agda-proven | Proofs-first (Phase 1) | +| Betlang | Experimental | Concept | +| Ephapax | Experimental | Concept | +| Phronesis | Ethical AI specification DSL | Concept v0.1 | +| Eclexia | Resource-first DSL | Concept v0.1 | +| Oblíbený | Secure-enclave DSL | Concept v0.1 | +| Anvomidav | Hard real-time DSL | Concept v0.1 | +| WokeLang | Human-centric DSL | Concept v0.1 | + +KitchenSpeak is the only member of the family with active Agda proof work +(proofs lead implementation — the Agda-Proven invariant per ADR 0001). + ## Anti-Purpose This project is NOT: diff --git a/contractiles/must/Mustfile.a2ml b/contractiles/must/Mustfile.a2ml index bd5f01b..16230f6 100644 --- a/contractiles/must/Mustfile.a2ml +++ b/contractiles/must/Mustfile.a2ml @@ -24,6 +24,33 @@ that MUST hold at all times. - run: test -f README.adoc || test -f README.md - severity: critical +## KitchenSpeak + +### agda-proven-invariant +- description: KitchenSpeak proofs directory must exist (proofs lead implementation) +- run: test -d kitchenspeak/proofs/agda +- severity: critical + +### kitchenspeak-lib-declared +- description: kitchenspeak.agda-lib must declare echo-types dependency +- run: grep -q 'echo-types' kitchenspeak/proofs/agda/kitchenspeak.agda-lib +- severity: critical + +### kitchenspeak-postulates-annotated +- description: All Agda postulates must be preceded by -- AXIOM: comment (trusted-base governance) +- run: "! grep -n '^postulate' kitchenspeak/proofs/agda/*.agda | grep -v 'AXIOM' || true" +- severity: warning + +### kitchenspeak-proof-needs-present +- description: PROOF-NEEDS.md must enumerate postulate trusted base +- run: test -f kitchenspeak/proofs/PROOF-NEEDS.md +- severity: critical + +### kitchenspeak-adr-echo-attachment +- description: ADR 0004 (Echo attaches to Linear/Dyadic) must be present +- run: test -f kitchenspeak/decisions/0004-echo-attaches-to-linear-dyadic.adoc +- severity: critical + ## Banned ### no-hardcoded-paths