A formally-verified, hardware-agnostic orchestration DSL for the domestic kitchen. Translates culinary expert intent (Chef Personas) into machine-executable actions for MQTT/Matter-class appliances, while maintaining physical and digital safety through a multi-layered type system.
Status: v1.0 specification stable (the original class teaching artefact). v2.0 elevation in progress — a physically-grounded type system, a reference compiler, and a machine-checked material-safety proof. Not intended for deployment on actual kitchen hardware yet.
v2.0 turns typing into the superpower: physical safety lives in the type system, so a program that could curdle the milk, scorch the egg, bake the silicone spatula, or over-torque the robot arm fails to compile. Materials carry thermal/mechanical/chemical safety envelopes; appliances carry capability envelopes; an action type-checks only inside the intersection of the two. The same types lower to machine-checked Agda proofs and to a HAL over Matter / MQTT / ROS 2.
Start at docs/design/0000-blueprint-index.adoc (the document map and the
"golden thread" tracing no-curdle from syntax → type rule → proof → HAL).
# Build and run the reference compiler (dependency-free OCaml; needs dune).
cd src/compiler && dune build
KSC=_build/default/main.exe
$KSC check ../../examples/v2/poached-egg.ks # => OK
$KSC check ../../examples/v2/negative/curdle-milk.ks # => error [CURDLE] ... (exit 1)
$KSC lower --target matter ../../examples/v2/poached-egg.ks # => Matter trace JSON
# Run the full accept/reject corpus (14 cases):
bash tests/run-corpus.sh
# Machine-check the v2.0 flagship safety proof:
make -C proofs nocurdle # (or: agda proofs/agda/NoCurdle.agda)Not intended for deployment on actual kitchen hardware. Experimental companion to the other languages in this repository.
KitchenSpeak is an experimental DSL designed as a teaching vehicle for advanced type theory (linearity, session types, refinement types, effect systems, dependent types) in an applied, tangible domain. The v1.0 specification was written by the student cohort themselves as a requirements-engineering exercise under a second instructor, and offered to the type-theory stream as the target language for the term’s proof work.
| File | What it is |
|---|---|
|
The class’s v1.0 specification, reproduced verbatim. Authoritative requirements artefact for the term. |
|
The class’s grammar (Section A) plus three minimal additive patches (Section B) closing productions that the class referenced but did not define, and constructs illustrated in worked examples that had no production at all. Every patch is marked; nothing rewrites the class’s work. |
|
Type-theoretic companion. Maps each of the class’s seven types onto
standard foundations (linear logic, session types, refinement types,
effect systems, units of measure, postulated oracles) and names each
load-bearing proof obligation. Separate from |
|
Worked example. The minimum KitchenSpeak program that exercises all three of Linear (the egg), Tropical (the water temperature), and Echo (the visual witness). Heavily commented as a teaching artefact. |
|
Architecture Decision Records (ADRs). One per material decision on how KitchenSpeak lowers, tools, or targets other systems. |
|
Proof-assistant lowerings of the worked examples. Agda is the v1.0
target (see ADR 0001). Room for a future |
From SPEC.adoc §2, with formal foundations elaborated in COMMENTARY.adoc:
-
Tropical (
~) — range and gradient. Refinement type over a quantity with a bounded derivative. -
Linear (
←) — resource consumption. Linear logic; an egg cannot be used twice. -
Choreographic (
sync) — concurrency and sequencing. Session-typed multiparty barriers. -
Echo (
@) — sensor feedback. Postulated oracle that witnesses the physical world. -
Dyadic (
<~>) — irreversible binding. Tensor product in linear logic; flour and water become dough. -
Ceremonial (
ceremony) — social context. Ambient effect / reader-monad-style pacing and priority. -
Primitive — SI-unit-indexed physical quantities.
Every step in a KitchenSpeak program carries:
-
max_duration— a wall-clock timeout. Termination witness. -
on_fail— one ofABORT,RECOVER,WARM. Total failure handler. -
proving(on the enclosingsync) — names the echo witness that certifies block completion. Existential witness binder.
Together these make every sync_block a total function into
{success} ⊎ {aborted, recovered, warmed}, with termination discharged
by a well-founded measure on the timeout.
-
Zero Scams — all echoes resolve against local sensors; no cloud round-trips for safety-critical witnesses.
-
Chef Orchestration — multi-actor
syncacross heterogeneous hardware. -
Agda-Proven — zero unresolved goals in the core proof library for the canonical recipes (Dough, Emulsion, Sear).
Read in this order for a 20-minute orientation:
-
SPEC.adoc§1–§3 — what the class built and why. -
examples/poached-egg.ks— the smallest program that exercises Linear + Tropical + Echo together. -
grammar.ebnf— Sections A then B. -
COMMENTARY.adoc§The seven types — formal foundations, one per type.
-
A lexer specification (the placeholder nonterminals in
grammar.ebnf§O3 are deferred to a later revision). -
A verified classifier story for echo-types — v1.0 treats them as postulated.
-
A committed choice between Agda and Coq.
SPEC.adoc§4 names both;COMMENTARY.adocuses Agda throughout for pedagogical tractability. -
A committed wire protocol.
SPEC.adoc§5 names HomeConnect, SmartThings, Tuya; Matter and MQTT are candidates for a later HAL revision.
KitchenSpeak is experimental and not part of the core ten-language
portfolio described in EXPLAINME.adoc. It shares design DNA with
several siblings:
-
Linear semantics are related to
affinescript/andephapax/. -
Session-typed choreography overlaps with `anvomidav/’s real-time model.
-
Effect / ceremony separation echoes `eclexia/’s constraint-propagation approach.
-
Resource-counting discipline is cousin to
contractiles/.
None of these dependencies are hard — KitchenSpeak is a self-contained teaching DSL.