CHOREOGRAPHIC PROGRAMMING · COMPILED TO A PROTOCOL CONTRACT
Two voices.
One melody.
Hocket is a versioned, machine-checkable protocol contract — a flat JSON state machine regenerated from a choreography like a lockfile. Born of Ryo's choreographic RFC, but bound to no language: every endpoint runs a generated monitor against the same artifact, so a Rust service, a Swift client, and a TypeScript stub can prove they speak the same protocol.
Choreographic programming writes the whole interaction as one program over role-typed values; the compiler projects it into per-role endpoints. In medieval music, a hocket is two voices alternating single notes — each silent exactly where the other sounds. That is endpoint projection itself.
each voice is silent exactly where the other sounds sha256:9f2c…e41a
One artifact
A single .hocket document — roles, states, message schemas, error
vocabulary — canonically hashed with JCS (RFC 8785). Same choreography → same
contract → same hash, no matter who exported it.
Every endpoint checked
Each role runs a generated FSM monitor over its own projection. No lock-step, no implicit synchronization — transfers and branch tags carry everything.
Sequence & shape, never semantics
A contract proves the client sent PaymentAuth at the right time with
the right fields — not that charge() charged the right amount.
Any language, same protocol
Rust, Swift, Kotlin, TS — Ryo is the origin, not a requirement. The monitor verifies peers against golden CBOR traces; conformance is judged over the wire, not by shared code.
Operational semantics, played live
The Payment choreography under its monitors. Each role's monitor holds just
(session_id, current_state) and checks every event against its own projection —
a matching transfer advances it; at a choice it doesn't own it blocks until a branch tag
arrives; anything else is ProtocolViolation {expected, got, state}, session over.
Auto-run the session, or step it yourself as the Client decider — and break the contract
on purpose to meet the violation yourself.
Monitors check sequence and shape, never semantics — that the client sent
PaymentAuth at the right time with the right fields, not that
charge() charged the right amount. Failures are named from a closed vocabulary,
fixed in v0.1: TransferFailed (transport error mid-transfer) ·
Timeout (bounded wait exceeded) · ProtocolViolation (contract
breach by the peer) · Aborted (scope cancellation) — extensions go through
contract versioning, never ad-hoc strings.
Anatomy of the contract
The exported Payment contract. Hover any line to read the rule it answers to.
The opening handshake
First frame on any transport, both directions. Pick a peer — the rule applies itself.
{
contract: "hocket/0.1",
protocol: "Payment",
version: "1.4.0",
contract_hash: "sha256:9f2c…e41a",
role: "Client"
}
{
contract: "hocket/0.1",
protocol: "Payment",
version: "1.4.0",
contract_hash: "sha256:9f2c…e41a",
role: "Server"
}
default)MinorDeterministic CBOR on the wire
Definite lengths, canonical integer and key ordering — deterministic bytes make golden traces byte-stable. JSON is permitted for debugging only; conformance is judged on CBOR.
The schema vocabulary is deliberately tiny: bool u32 u64 i64 f64 str bytes
list[T] map[str,T], records, enums. It maps 1:1 onto Swift / Kotlin / TS stubs.
Conformance by golden traces
For every path through the graph — cycles cut after one traversal — the exporter emits
the exact CBOR frame sequence each role must produce and accept, including the HELLO and
the ProtocolViolation cases.
A foreign implementation is conformant if it passes all traces for its claimed role over the TCP binding.
Transport bindings
Ordered, reliable, framed delivery per session. Branch tags ride the same ordered stream —
a lost tag is indistinguishable from connection failure, which the fixed failure
vocabulary already covers as TransferFailed or Timeout.