Hocket

Versioned, machine-checkable protocol contracts — born of Ryo choreographies, open to any language.

Hocket originates in the choreographic-programming model proposed in RFC: Choreographic Protocols for Ryo: one program over role-typed values (T @ Role), projected to endpoints by the compiler. But the .hocket contract it defines is bound to no language — it is a flat JSON state machine that any implementation, in any programming language, can monitor itself against and verify its peers with, over the wire.

Hard rule zero: the contract is build output, never source. It is regenerated from the choreography like a lockfile. Any hand edit invalidates it.

Documents

File	Contents
hocket-0.1.md	The hocket/0.1 specification — document format, operational semantics, versioning, handshake, encoding, transports, conformance

Interactive walkthrough of the protocol (live monitor playground, contract anatomy, handshake rules, session tickets and the HTTP profile): hocket.ryolang.org.

The shape of it

• One artifact. Roles, states, message schemas, error vocabulary — canonically hashed with JCS (RFC 8785). Same choreography → same contract → same hash.
• Every endpoint checked. Each role runs a monitor holding just (session_id, current_state) over its own projection of the graph.
• Sequence and 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. Ryo is the origin, not a requirement. Conformance is judged by golden deterministic-CBOR traces over the wire, not by shared code — Rust, Swift, Kotlin, TypeScript, or anything else with a CBOR library.
• Sessions that survive the wire. The monitor's whole state is one small cursor, serializable into an opaque ticket: resume after drops, deploys, or process migration — even mid-choice, even around a guarded back-edge. Expiry is wall-clock, never connection lifetime.
• HTTP as a first-class profile. One POST per transition, ticket in a Hocket-Session header, ordering enforced by the ticket rather than the transport; duplicates are idempotently ignored. Streams remain canonical.

Status

Draft 0.1, pre-implementation. The state machine, the handshake, and session resumption are stable inputs to the v0.1 implementation; the sequence-level evolution calculus, ticket signing, and the contract registry are open work (§13 of the spec).

References

Hocket stands on the choreographic-programming and session-types literature — the model is theirs; the language-agnostic, machine-checkable contract is ours.

• Fabrizio Montesi, Introduction to Choreographies (Cambridge University Press, 2023) — the systematic foundation: choreographies, endpoint projection, knowledge of choice.
• Carbone & Montesi, "Deadlock-freedom-by-design" (POPL 2013) — choreographic programming proper; the theory behind the single-decider rule and guarded back-edges.
• Honda, Yoshida & Carbone, "Multiparty Asynchronous Session Types" (POPL 2008) — global types, local types, projection: the ancestor of the contract graph and its per-role monitors.
• Giallorenzo et al., "Multiparty Languages: The Choreographic and Multitier Cases" (ECOOP 2021) — the isomorphism between global protocols and role-annotated programs.
• Choral (JVM), ChoRus (Rust), HasChor (Haskell) — choreographic languages and libraries whose compiled endpoints could verify themselves against a .hocket contract.

The full annotated list, with what each work contributes to the spec, is Appendix C of hocket-0.1.md.

Author

Pepe Navarro — creator of Ryo.

License

This specification is licensed under CC BY 4.0. Implementations of the protocol — in any language — are explicitly welcome and are not derivative works of this text.