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, seq) — the cursor, serializable into a ticket (§8) —
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 (wall-clock session expiry — never connection loss) · 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",
session_id: "7f3a…91c2", ← minted here
expires_at: 1786000900, ← now + session_ttl
resume: null
}
{
contract: "hocket/0.1",
protocol: "Payment",
version: "1.4.0",
contract_hash: "sha256:9f2c…e41a",
role: "Server",
session_id: "7f3a…91c2", ← echoed verbatim
expires_at: 1786000900, ← echoed verbatim
resume: null
}
The initiator mints session_id and computes
expires_at = now + session_ttl (fixed by the contract, covered by the hash);
the peer echoes both — agreement, not coincidence. A mismatched echo is
ProtocolViolation at state 0.
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. Resume-after-drop, duplicate delivery, and stale
or expired tickets are trace cases too.
A foreign implementation is conformant if it passes all traces for its claimed role over the TCP binding.
Session tickets — the cursor, serialized
Monitor state is one small tuple; its serializable form is an opaque
ticket — contract_hash · session_id · state_id · seq · nonce ·
expiry. Present it after a drop, a deploy, or a process migration and the session
resumes exactly where it stood — even mid-choice, even around a guarded back-edge.
A stale or forged ticket is a ProtocolViolation; an expired one is a
Timeout. A session dies by expiry, never by transport loss.
HTTP, a first-class profile
One POST per transition, body unchanged — deterministic CBOR. The ticket rides in a
Hocket-Session header and is the ordering: a mismatched state is a
ProtocolViolation, a duplicate POST is idempotently ignored.
Advisory Hocket-* headers — protocol, contract hash, state, seq, msg,
role, kind, expiry — plus a standard Idempotency-Key let gateways
route, meter, and dedupe without parsing CBOR or decoding the ticket.
What it cannot do: long-lived blocking waits and server push stay stream-only. Streams remain canonical.
Transport bindings
Streams are canonical: 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. Every profile speaks tickets, so a session can cross transports
without dying.