dh — small enough to verify, expressive enough to run a business
A Datalog extension for declaring ontologies: relations, rules, invariants, and relays. Deliberately not Turing-complete — dh stays inside logic fragments where composition, decidability, and cost envelopes are mathematical consequences, not hopes.
The only path from a model's output to the world
LLM output lands in relay namespaces — candidate.* for extractions, proposal.* for actions. No rule may derive accepted truth or an executable intent directly from them.
Promotion happens only through an acceptance rule a developer wrote and can inspect — here, a bounds check and a ratification gate. Your agent writes this file; tarski verify tells it whether the contract holds.
-- fallible sensor: the voice parser proposes, nothing more relay candidate.order(item, qty) from tool voice_parse -- acceptance: promotion is an inspectable rule, not a vibe order.line(item, qty) :- candidate.order(item, qty), menu.bounds(item, max), qty ≤ max. -- out of bounds → stage and ask, never submit prompt.confirm(item, qty) :- candidate.order(item, qty), menu.bounds(item, max), qty > max. -- the wall: named, enforced at every fixpoint invariant pos_only_accepted_lines never pos.ticket(item, qty) without order.line(item, qty).
What the fragment buys you
The simplicity developers feel is the surface of structural properties underneath. Because dh stays inside well-behaved fragments of logic, the platform can check things about your system that general-purpose code cannot offer.
Bounded blast radius
What any change can affect is bounded by the rule graph's neighborhoods. Recomputation, hydration, and review scope to what a change can actually reach.
Modules that merge safely
Namespace boundaries are computed from the ontology and checked by the platform. Independently developed modules compose — or the merge is rejected with a verdict, before deploy.
Performance before profiling
The shape of a rule determines its worst-case cost. Tarski reports which rules leave the tractable classes — and why — before anything runs. A regression is a semantic diagnosis first.
Indexes and plans are derived from the ontology and declared queries. Tuning can trade constants; it can never trade meaning — every plan must reproduce the exact model and provenance the reference evaluator derives.
Designed to be written by agents, read by humans
You will rarely write dh by hand. Coding agents author it against your Scenarios and invariants, iterating on tarski verify until the contract holds.
What matters is that when you do read it — an acceptance rule during an audit, an invariant during sign-off — each statement is small, declarative, and means exactly what it says.