horos

Why it exists

The family deliberately left a gap. ontos says here is a value but is pre-schema by construction; logos reasons over values but stays agnostic to types, which enter only through its extension points, never its core. Neither owns the question and is it a well-formed T? — the form a value must satisfy to count as a thing of a kind. horos fills that gap, and only that gap.

Its move is to invent no new machinery. A type is a predicate; v : T is a checking question; so a type system is a body of rules — a constitution over logos, not a new engine. A descriptor T is an ordinary ontos value; a typing rule is a logos clause; checking conformance is logos check() over a derivation someone supplies. This makes horos the peer of thesmos: thesmos lays down the law of who may do what, horos the law of what counts as what — both check, neither searches.

A concrete example

A descriptor is just an ontos value under the reserved horos/ namespace. A closed record:

record closed
  field "name" req (scalar utf8-text)
  field "age"  opt (scalar int)

map{ "name": text("ada") } conforms — the required field is present, the optional one may be absent. map{ "age": int(36) } does not — the required name key is missing. map{ "name": text("ada"), "x": int(1) } does not — an extra key is forbidden under closed (the open/closed flag is mandatory; silent open-vs-closed is the classic schema-drift bug). The same DSL covers unions, atom refinements like atom-len 1 3, and guarded-recursive shapes such as a cons-list. Every judgment is total — it never throws; a non-conforming value is simply classified out.

What it unlocks

Because checking v : T is total, bounded, and search-free, a typed value can carry its own account — value + a derivation that v : T. Two services on the substrate agree on a contract not by trusting a shared registry but by re-deriving it against the same frozen horos constitution. The seam disappears, one layer up from ontos.

horos adds classification, never a new equality: two values are the same iff they are the same ontos value, the invariant every layer inherits. What it refuses, it hands to its proper home — type inference (searching for a derivation) is a separate runtime over logos, horos's stele-analogue; named-schema registration in spaces is thesmos's authority. horos says only "this value is a well-formed T."

What's next

The v1 form contract is frozen, and the tri-core reference implementation (core/{rs,go,ts}) with its byte-pinned conformance vectors has landed and is CI-gated — the three cores agree byte-for-byte. What v1 ships is a search-free structural recognizer with no logos dependency yet; the deferred logos check() interop (which decides the semantics/policy factoring) is blocked on a logos-contract release that pins the current ontos. The other open frontier is the build-on-demand structural subsumption relation S <: T — specified, but added only on a concrete consumer need.