Prologue: Three Attempts

Here is a sentence from the world I work in:

A trade must not clear if any beneficial owner of the counterparty, at any depth, appears on a sanctions list.

A regulator can write that sentence. A compliance officer can read it. A new hire understands it on day one. Now try to find it in the codebase.

In every trading system I have seen — including the ones I built — that sentence does not live anywhere. It is smeared. There is a recursive ownership walk in the onboarding service. There is a nightly job that flattens the ownership graph into a cache, because the walk was too slow to run per-trade. There is a depth limit of three in the risk engine, added by someone who feared cycles and never removed. There is a hotfix from two years ago that special-cases one counterparty, with a comment that says // see JIRA-4711, and JIRA-4711 was deleted in a migration. Ask “where do we enforce the sanctions rule?” and the honest answer is: everywhere, and therefore nowhere.

This is not a story about bad engineers. The engineers were good. It is a story about writing rules in languages built for procedures. Java, C++, and their relatives are magnificent at describing how: fetch this, loop over that, update the other. The sanctions sentence contains no how at all. It is pure what — a statement about which facts must hold. Translating what into how is a lossy compilation step, and we perform it by hand, under deadline, and then we maintain the compiled output forever while the source — the sentence — lives only in a PDF and in shared tribal memory.

I have come to believe that every trading system is a logic program, implemented badly, by hand, by people who were never told that’s what they were doing. Compliance is rules. Risk limits are rules. Order routing is rules. Margin, netting, eligibility, settlement — rules, rules, rules. We encode them as control flow, and the control flow slowly eats them.

Before settling on that diagnosis, I tried two others — each a real project, each built to test a theory of what was missing.

Attempt one: the engine is the problem

The first theory was that the machinery was missing. Rules engines existed — CLIPS, the classic expert-system shell, has been matching rules against facts since the 1980s — but nothing in that lineage could live inside a trading system, where the budget per event is measured in microseconds. So I rebuilt one. The project, reclips, was a clean-slate reengineering of the CLIPS shell: same rule-matching idea, new body — columnar fact storage, a delta-based matcher, preallocated memory, deterministic replay, latency you could put on a hot path.

The engine worked. And working, it taught me what the actual problem was. When you feed a classic rule engine a set of rules, the answer you get can depend on the conflict-resolution strategy — the policy that decides which rule fires first when several match. CLIPS ships seven of them. Seven. Think about what that means: the rules alone do not determine the answer. The rules plus a scheduling policy determine the answer. Your knowledge doesn’t mean anything by itself; it means something only in the company of an execution order. I had built a very fast machine for evaluating programs that had no fixed meaning.

Attempt two: the hardware is the problem

So I went the other way. If I couldn’t fix what programs mean, I could at least fix what they cost. The next project, an ahead-of-time compiler for reactive dataflow programs, knew things about hardware that most programmers politely ignore: cache-line geometry, NUMA placement, huge pages, the price of a branch. It compiled event-processing pipelines down to code that respected physics.

It worked too. The systems got faster. They did not get one bit clearer. The sanctions sentence was still smeared across services — the smear now executed in fewer nanoseconds. Fast confusion is still confusion, and speed had never been why the rule took a hotfix and a dead JIRA ticket to enforce.

Neither project was wasted — an engine and a compiler are correct answers to the questions they ask, and both still earn their keep. But neither question was this question. The missing piece was a language: one where the regulator’s sentence is the program — not the inspiration for the program, the program — where the order you write things in cannot change what they mean, and where every answer can show its work, because in a regulated industry an answer without a pedigree is a liability.

The old idea

Here is the uncomfortable part: that language already exists, and it is fifty years old. Logic programming — writing programs as facts and rules and letting an engine derive the consequences — carries a history of spectacular promise and two spectacular collapses, including the largest state-funded bet on a programming paradigm ever made. Chapter 2 tells that story properly, because if I’m asking you to take this idea seriously in 2026, I owe you an honest account of why it failed in 1992.

But two things have changed since then, and they change everything.

The first is hardware. The old logic languages were built around a sequential search procedure that fights modern silicon at every step. The branch of the family this book is about — Datalog — computes by a different scheme, one that is embarrassingly parallel by nature. For decades that was a curiosity. Then the machine-learning boom filled the world with GPUs. The hardware the paradigm always needed got built, at planetary scale, for someone else’s reasons.

The second is language models. LLMs write code now — yours and mine — and they write it fluently, confidently, and sometimes wrongly, and the bottleneck of software has quietly moved from writing to verifying. That inverts what we should optimize a programming language for. For fifty years we optimized languages for the writer. A language optimized for the checker looks different: small, declarative, order-independent, with answers that carry their own derivations. It looks, in fact, like a logic language — which suggests these fifty-year-old ideas were not wrong, just early.

This book stands on that inversion, and its argument fits in one sentence: let the language model propose the rules, let a symbolic core guarantee what follows from them, and let the GPU make it fast.

The third attempt

The second half of this book introduces Strata-K, a logic language I am building in the open — the third attempt, the one aimed at the actual missing piece.

I want to be precise with you about its status, here on the first pages, because the rest of the book depends on your trust. Today, Strata-K is a working reference implementation: the language core runs end-to-end on a CPU — parsing, checking, evaluation, exact probabilistic queries, an answer-set solver — and is cross-checked against an established independent engine and fuzzed against itself. The GPU engine is designed in detail and not yet built. Where this book describes what runs, you can run it: every code listing outside an explicitly marked “future” frame executes today, and every output shown is the real output. Where the book describes design, it says so in the open. There are no benchmark numbers for hardware that doesn’t exist yet, here or anywhere.

What I ask of you is narrower than belief. You write C++, or Java, or something in their family, and somewhere in your current codebase sits your own version of the sanctions smear — the rule that is everywhere and nowhere. Hold that rule in mind for eleven chapters. The third attempt’s bet is that by the end you will want to write it down as what it is.

Chapter 1 — The Idea: What, Not How

A loop you have already written

Let’s start with work you have done before. A company can own another company, which can own another. Given the direct ownership links, compute ultimate control: who sits above whom, at any depth. This is the skeleton of the sanctions rule from the prologue, and it is also — strip away the domain — plain transitive closure, a computation you have implemented more times than you can count: build dependencies, org charts, network reachability, #include graphs, GC root scanning. It is always the same loop.

In Java it comes out something like this:

Set<Edge> controls = new HashSet<>();
Deque<Edge> work = new ArrayDeque<>(owns);

while (!work.isEmpty()) {
    Edge e = work.pop();
    if (!controls.add(e)) continue;          // already known
    for (Company next : ownsIndex.get(e.to()))
        work.push(new Edge(e.from(), next)); // extend to the right
}

Ten lines, and you could write them half asleep. Now look at what those ten lines quietly demand of you.

The continue on the duplicate check is load-bearing: remove it and cyclic ownership — which absolutely occurs in real corporate structures, usually on purpose — loops forever. The choice to extend edges only “to the right” is load-bearing too. Is right-extension alone actually sufficient, or do you also need to join derived edges with each other? For this particular problem, right-extension suffices — but that’s a small theorem, and you proved it in your head, and you wrote the proof down nowhere. The next maintainer gets the loop, not the theorem. And there’s a third demand, the expensive one: this code computes the answer once. When tomorrow’s onboarding adds three ownership links, recomputing from scratch is wasteful, so someone will eventually write the incremental version — and the incremental version is a genuinely different and harder program, with its own theorem, also unwritten.

None of this is the problem statement. “Who ultimately controls whom” says nothing about worklists, visited sets, extension direction, or increments. All of that is how. You supplied it, by hand, because your language cannot say what.

The same program, as what

Here is the whole thing in Strata-K:

domain company.
pred owns(company, company): Bool.
pred controls(company, company): Bool.

controls(X, Y) :- owns(X, Y).
controls(X, Z) :- owns(X, Y), controls(Y, Z).

owns(apex, brightwater).
owns(brightwater, cobalt).
owns(cobalt, dunlin).

Read the two middle lines aloud; the syntax is designed to be read aloud. The symbol :- is “if”, the comma is “and”, capitalized names are variables, lowercase names are concrete things:

• X controls Y if X owns Y.
• X controls Z if X owns some Y, and that Y controls Z.

That’s the entire logic — two sentences a compliance officer could check against the regulation. The lines below them are facts: Apex owns Brightwater, Brightwater owns Cobalt, Cobalt owns Dunlin. The lines above are rules: sentences with variables, true for any companies you substitute in. Facts are your data. Rules are your knowledge. There is no third thing.

Run it:

$ strata run examples/book/ch01-ownership.strata
controls(apex, brightwater)
controls(apex, cobalt)
controls(apex, dunlin)
controls(brightwater, cobalt)
controls(brightwater, dunlin)
controls(cobalt, dunlin)
owns(apex, brightwater)
owns(brightwater, cobalt)
owns(cobalt, dunlin)

Every ownership fact we stated, plus every control relationship that follows from what we stated. Apex controls Dunlin through a chain three deep, and nobody wrote a loop.

What the engine actually does

No magic is about to be revealed, and that’s the point — you already know the algorithm, because you’ve written it by hand.

The engine takes the rules and applies them to the facts it has. X controls Y if X owns Y — so all three owns facts produce three controls facts. Then it applies the rules again, to everything it now knows: the second rule can now combine owns(apex, brightwater) with the freshly derived controls(brightwater, cobalt) to conclude controls(apex, cobalt). Then it applies the rules again. At some point a full pass derives nothing it hasn’t already got — and it stops, because if a pass adds nothing, every future pass adds nothing too.

That’s a do-while loop. Yours, in fact — the worklist code above is this exact scheme, hand-compiled for one specific pair of rules. The stopping point has a name, and it’s the first vocabulary word of this book worth memorizing: the fixpoint — the state where applying every rule yields nothing new. “Run the program” means “find the fixpoint.” Your while (!work.isEmpty()) was a fixpoint computation all along; you just weren’t given the word, or the machine that owns the loop for you.

Two guarantees come with handing the loop over, and both would have been your bugs to make.

It always terminates. Look at the right-hand side of the rules: variables, and nothing else. There is no new. A rule can only combine constants that already exist — it can conclude controls(apex, dunlin), but it cannot mint a company that was never mentioned. A finite set of companies has a finite set of possible controls facts, the engine only ever adds facts, so the loop provably stops. Cycles in the data? Apex owns Brightwater owns Apex? The engine derives that each controls the other — and stops. The infinite loop you guarded against with that load-bearing continue is not merely handled; it is impossible to express.

Order doesn’t matter. Swap the two rules. Shuffle the facts. Split them across ten files and load them in any order. The fixpoint is the same set of facts, every time — not as a matter of engine politeness, but of arithmetic: the answer is defined as everything derivable from what you stated, and derivability doesn’t care what line something was written on. Hold this property; it looks like a convenience and it is actually a foundation. Order-independence is what died in the older logic languages (chapter 4 does the autopsy), and it is what makes machine-generated rules checkable at all (chapter 9 builds on it).

What, not how

Notice everything the Strata-K program does not say. It does not say to walk the graph left to right. It does not maintain a visited set. It does not choose breadth-first against depth-first. It does not schedule. All of that — the entire content of your ten Java lines — has become the engine’s problem, and the engine is free to solve it well: to pick join orders, to index, to process only the delta (the facts new since the last pass — the trick that turns naive rule-running into something competitive, and, much later in this book, into something massively parallel).

You have seen this trade before, and you liked it. SQL made exactly this move for lookups: you write WHERE customer.id = order.customer_id, and the planner — not you — decides hash join or index scan. Nobody mourns the hand-rolled B-tree traversals. Logic programming is the same bargain extended from lookup to inference: not just “find the rows where”, but “find everything that follows from”. And your database has, in fact, already smuggled a fragment of this paradigm into production behind your back — WITH RECURSIVE, the SQL feature everyone writes once, gets wrong twice, and wraps in a comment begging nobody to touch it, is precisely this chapter’s two rules wearing a straitjacket. Chapter 3 returns to that.

There is a deeper consequence, easy to miss. The Java version is a function: it computes controls, and if next month you need “which companies does nobody control” or “how many entities sit under Apex”, you write more functions, each with its own loop, its own bugs, its own theorem. The Strata-K version is knowledge: the two rules define what control means, and any number of questions can be asked against that same definition. New requirement, new rule or new query — not a new algorithm. The program stops being a pile of procedures that happen to agree and becomes a single model of the domain that answers questions. That is what “program = knowledge” means, and it’s why the sanctions sentence from the prologue can be the program instead of the program’s lost inspiration.

One more thread, planted here, paid off in chapter 7: because the engine derives every fact mechanically from stated facts and rules, it can remember how — every derived fact has a pedigree. When compliance asks “why was this trade blocked?”, the answer is not “attach a debugger”; the answer is the derivation chain itself: blocked because controls(apex, dunlin), because owns(apex, brightwater) and owns(brightwater, cobalt) and owns(cobalt, dunlin), and dunlin is listed. An answer that shows its work. This book’s title lives in that sentence.

What this is not

A short honesty section, because “the engine figures it out” has burned you before.

This is not AI, in the current sense of the word. Nothing here is learned, statistical, or approximate. The fixpoint is deterministic mathematics — same facts, same rules, same answer, bit for bit, forever. (The connection to LLMs, this book’s real motivation, is division of labor, not fusion: the model proposes rules; this machinery guarantees what follows. That story is chapter 9’s.)

This is not a general-purpose language, either. You cannot write a web server in it, and that is a feature bought deliberately: the no-new restriction that guarantees termination costs expressive power, and the language spends that coin on purpose. Chapter 6 begins the tour of what the restriction buys and where the boundary actually sits.

And it is not a silver bullet. Most of your codebase is legitimately procedural and should stay imperative. The claim is narrower and sharper: the rules buried in that codebase — compliance, limits, routing, eligibility — are logic programs today, written in a language that can’t see them. They deserve a language that can.

The idea, and the question it raises

One chapter, four words of vocabulary, and the whole paradigm is on the table:

A program is a set of facts (data) and rules (knowledge). Running it means deriving everything that follows — computing the fixpoint. A query asks about the result. You state what; the engine owns how.

Everything else in this book — the pluggable arithmetic that turns the same rules into costs and probabilities, the layered negation, the self-consistent choice models, the GPU story — is this idea, compounded.

Which leaves the question you should be asking: if it’s this simple, this old, and this good, why isn’t the world already written in it? Fifty years of programmers were not fools. Something went wrong — twice, expensively, once with a superpower’s national budget behind it. That story is next, and Strata-K makes no sense without it.

Try it. Clone the repo, then:

cargo run -p strata-cli -- run examples/book/ch01-ownership.strata

Add owns(dunlin, apex). — a real circular structure — and run again. Note what does not happen.

Chapter 2 — Two Winters, Three Bets

Programming paradigms rarely die of being wrong. They die of being early, of being oversold, or of being welded to the wrong hardware — and logic programming managed all three, twice. This chapter is the honest account I promised: where the idea came from, what was actually bet on it, why the bets failed, and why the failures tell you surprisingly little about the idea. If you’ve ever dismissed this field with “wasn’t that the thing from the eighties?”, this chapter is for you, because yes — it was the thing from the eighties, and the eighties are precisely what needs explaining.

1965: inference becomes mechanical

The story starts with a theorem about theorems. In January 1965, J. A. Robinson published “A Machine-Oriented Logic Based on the Resolution Principle” — a demonstration that logical deduction could be reduced to a single mechanical rule, resolution, simple enough for a computer to apply blindly and complete enough that anything provable could, in principle, be reached by it. Before Robinson, formal logic was something mathematicians did to programs from the outside. After him, deduction was an algorithm.

It is hard to overstate what this seemed to promise. If deduction is mechanical, then knowledge plus compute equals answers: state what you know, ask what you want, let the machine grind out what follows. Every system in this book — including the one in the repository this text ships with — is downstream of that promise. So, in a real sense, is every SQL query you have ever written.

The catch surfaced immediately, and it has a name you know from your own work: combinatorial explosion. Resolution is complete the way brute force is complete. Blind search through the space of derivations drowns in itself long before it proves anything interesting, and by the early seventies it was clear that “logic plus compute” was not enough; you needed logic plus compute plus control over where the search goes.

Bet one: logic as a programming language

The response was one of the great moves in the history of programming languages. In Marseille around 1972, Alain Colmerauer and Philippe Roussel built a system for processing natural language; in Edinburgh, Robert Kowalski was developing the theoretical reading that made it a language. Their converged insight: don’t search blindly — restrict attention to rules of the form “conclusion if conditions” (Horn clauses, though we won’t need the term again), read them procedurally — to prove the conclusion, prove the conditions, left to right — and suddenly resolution stops being a search through chaos and becomes something a programmer can steer. They called the system Prolog, programmation en logique. Roussel wrote the first interpreter in ALGOL-W; within a decade there were dozens.

Kowalski crystallized the philosophy in a 1979 paper whose title is the cleanest slogan the field ever produced: “Algorithm = Logic + Control.” Every algorithm decomposes into a logic component — what the problem is — and a control component — how to search for the answer. Separate them, and you can improve the how without touching the what. It is the exact bargain I offered you in chapter 1, and it was on the table before most of this book’s readers were writing code.

And Prolog worked. On the hardware of its day it worked startlingly well — David Warren’s 1983 abstract machine design compiled it tightly enough to embarrass the skeptics — and through the early 1980s Prolog was, alongside Lisp, one of the two serious languages of artificial intelligence. The what-not-how dream had a working vehicle. The vehicle had a flaw, and the flaw was structural: Prolog achieved its efficiency by fusing logic and control back together — clause order, goal order, and the cut all make the search procedure part of the program’s meaning. Chapter 4 dissects that fusion with a running example; for now, note only the irony. The language born from “Algorithm = Logic + Control” shipped the two welded.

Bet two: a superpower buys the hardware

By 1982 the idea had enough momentum to attract the largest wager ever placed on it — arguably the largest state wager ever placed on a single programming paradigm. Japan’s Ministry of International Trade and Industry founded ICOT, the Institute for New Generation Computer Technology, under Kazuhiro Fuchi, and launched the Fifth Generation Computer Systems project: a ten-year national program to leapfrog the American computer industry not by building faster conventional machines but by building a different kind of machine — one whose native operation was logical inference. Logic programming would be the machine language; performance would be measured not in instructions per second but in logical inferences per second; and the hardware — Parallel Inference Machines, programmed in a concurrent logic language called KL1 — would deliver the parallelism that sequential Prolog could not. Roughly ¥54 billion of government money — about $400 million, real money in 1982 — went in over the decade. Western governments, badly spooked, answered with crash programs of their own: DARPA’s Strategic Computing Initiative alone outspent FGCS, though it spread the money across AI broadly rather than one paradigm.

If you have never heard of any machine that came out of this, that is the outcome. The project ran its decade, built its prototypes — five PIM machines, a working KL1 toolchain, a research community — declared its results, and dissolved into a short follow-on; ICOT closed its doors in 1995. No industry adopted the machines. No successor generation was built.

The standard postmortem says Moore’s law killed it, and as far as it goes, that’s true: commodity microprocessors were doubling in speed on a rhythm no bespoke architecture could match. By 1992, an inference machine painstakingly designed for logic was slower than a general-purpose chip you could buy at retail — the specialized hardware was obsolete the day it worked. But hold the postmortem to the same standard as chapter 4’s autopsies and two deeper causes surface. First, FGCS bet on the wrong branch of the paradigm: KL1 was a concurrent dialect of the Prolog line — search-shaped, process-shaped — and extracting massive parallelism from it meant fighting the model, not riding it. The set-oriented, fixpoint-shaped branch of logic programming that is natively parallel existed by then only as database theory (we’re coming to it). Second, FGCS needed hardware built for logic, on a paradigm’s budget. What the field actually required — as the next forty years demonstrated — was hardware built for someone else’s problem at someone else’s scale, that logic could ride for free.

Understand that and you understand why this book exists. FGCS was right that logic programming’s future was massively parallel hardware. It was wrong about who would pay for the hardware, and it was three decades early. The congregation that waited for the messiah dispersed a generation before he arrived.

The winter

The collapse was general, and it was not FGCS’s fault alone. The specialized Lisp-machine market imploded in 1987, undercut by exactly the same commodity workstations. The corporate expert-system wave of the mid-eighties (chapter 4 examines the technology; chapter 2 only notes the business) crested and broke as the maintenance bills came due. FGCS wound down in 1992 with its goals visibly unmet. The years from roughly 1987 to 1993 are now called the second AI winter, and logic programming — which had let itself be marketed as the substrate of the coming machine intelligence — froze with the rest of the field. Funding stopped; research groups dispersed; “logic programming” became the phrase you removed from your grant proposal.

That is the stigma this book swims against, so let me be precise about what actually froze. What failed was a positioning: logic programming as the royal road to artificial intelligence, and as a reason to build exotic hardware. What never failed — what was barely even tested — was the narrower, humbler claim of chapter 1: that rules with a fixpoint semantics are a better way to write the rule-shaped parts of ordinary software. The winter buried both claims in one grave. Only one of them was dead.

Meanwhile, in the database department

Because here is the part the winter narrative always omits: through the entire boom, collapse, and freeze, a different community was quietly working on the other branch — the one FGCS didn’t bet on.

Database theorists had been circling logic-as-queries since a 1977 workshop on logic and databases; sometime in the mid-eighties the fragment they cared about acquired a name — Datalog, coined by David Maier — and through the late eighties it became the most-studied object in database theory. Datalog is what you met in chapter 1: rules over finite data, no term construction, guaranteed termination, order-independent fixpoint semantics. Perfect parallelizability sat in the definitions, untouched, because in 1988 nobody had parallel hardware worth the trouble. The running joke — Datalog as the field with a thousand theorems and no applications — had real teeth; the theory outran any deployment by a decade. But the theorems were the point. The evaluation algorithms (chapter 1’s delta trick among them), the negation semantics (chapter 6 uses it), the complexity bounds — the entire load-bearing frame of this book’s Part II was poured, as theory, during the winter, by people the AI collapse never touched.

The winter years kept producing at the semantic frontier too. Stable models — the meaning of unrestricted negation, the foundation of chapter 8’s @asp layer — date to Gelfond and Lifschitz, 1988: the paradigm’s deepest semantic result, published into the teeth of the collapse. Constraint logic programming was laid out by Jaffar and Lassez in 1987. The paradigm’s obituary and its best theorems share a decade.

The quiet revival

The thaw, when it came, came from engineering, and it came Datalog-shaped. In 2004, Whaley and Lam showed that a hard, valuable program-analysis problem — context-sensitive pointer analysis for real Java programs — could be specified in Datalog and solved efficiently, the specification an order of magnitude smaller than the hand-coded analyzers it replaced. Rules about code, deriving facts about code: the sanctions problem, for compilers. A research thread became an industry. Semmle (an Oxford spinout, 2006) built a company on a Datalog dialect for querying codebases; GitHub bought it in 2019, and its engine now scans code at world scale as CodeQL. Oracle Labs, needing to analyze enormous codebases, built the open-source Soufflé engine (2013–2016) — the same engine this book’s reference implementation tests itself against. LogicBlox built a commercial Datalog platform whose retail-planning deployments passed through Predictix into Infor; its lineage continues today at RelationalAI. Datomic (2012) put a Datalog query language at the heart of a production database and ended up owned by a bank running it for a hundred million customers.

Notice three things about this list. Every entry is from the fixpoint branch, not the search branch — the revival vindicated the wing of the family that the winter’s flagship bet passed over. Every entry survived by not calling itself logic programming — more on that camouflage in the next chapter. And every entry runs on stock hardware: the revival asked nothing of the machine that the machine wasn’t already selling. The paradigm came back exactly where its guarantees — termination, order-independence, analyzability — were worth money, and nowhere else.

Bet three

Which brings us to now, and to the wager this book is a brief for. Two things have changed since 1992, and neither was done for logic programming’s benefit — which is precisely why they can be trusted.

The first: the parallel inference machine got built. Not by a ministry, and not for inference — the deep-learning boom filled every datacenter and half the world’s desks with GPUs: massively parallel, memory-rich, commodity-priced, improving on a curve. FGCS’s hardware thesis, minus FGCS’s fatal clause. No one has to build hardware for the paradigm anymore; the paradigm has to meet hardware that already exists — and the fixpoint branch, unlike the search branch, meets it natively. (This is no longer hypothetical even in research terms: the first serious GPU Datalog engines have appeared in the last two years. Chapter 5 places them on the map, and chapter 10 takes up the architecture question in earnest.)

The second: the verification economy inverted. LLMs now write code — fluently, cheaply, and under no oath. When code is expensive to write, you optimize languages for writing it; that was every language war of the last fifty years. When code is cheap to generate and the scarce resource is confidence in what got generated, the language’s job flips: be easy to check — by machines, structurally, and by humans, readably. Chapter 4 grades the old logic languages on that axis and they fail it, badly, for reasons the winter never touched. But the paradigm — rules with order-independent meaning, answers that carry derivations — is the strongest candidate shape for a check-first language that we have. Fifty years of work on “how machines can trust conclusions” was waiting for a world with an oversupply of plausible text. That world arrived.

So the third bet is not the first bet retried — not logic as universal intelligence. And it is not the second retried — not bespoke silicon. It is smaller and harder-nosed than either: the rule-shaped fraction of real software, written as rules, checked as logic, running on hardware someone else already paid for, generated increasingly by models whose output nobody should trust unverified. The rest of this book cashes that sentence out. First, though — chapter 3 — let me show you how much of the bet is already, quietly, in production.

Chapter 3 — Dissolved, Not Dead

Chapter 2 ended with a claim that deserves suspicion: that the paradigm’s revival is already in production. “In production” is the phrase every dying technology clings to — somewhere, surely, a COBOL program still runs. So this chapter holds itself to a stricter standard: not museum pieces, but systems you — a working engineer in 2026 — have plausibly touched this month, that are logic programming under the hood. The thesis is in the title. Logic programming didn’t die; it dissolved. It survived everywhere rules matter more than process — but it survived in fragments, under assumed names, each fragment re-solving a piece of the same problem in isolation. The dissolution is a triumph for the idea and an indictment of the languages, and both halves matter to this book.

You pushed code today

If your repository lives on GitHub with code scanning enabled, then on your last push a logic program ran over your code. CodeQL — the engine behind GitHub’s security scanning — is a Datalog dialect in the direct lineage chapter 2 traced: your program is decomposed into a database of facts (this function calls that one; this value flows there), a vulnerability is a set of rules over those facts, and a finding is a derived fact, complete with the derivation. The scale is planetary and the fit is exact — “tainted data reaches a SQL string” is transitive closure with extra conditions, the very shape you wrote in chapter 1. The security analyst writing a CodeQL query is doing what the sanctions officer of the prologue could not: stating the rule as a rule and letting an engine find every instance.

The pattern generalizes far beyond GitHub. The academic result that reopened this field — Whaley and Lam, 2004 — was exactly this workload, and the Soufflé engine (the one this book’s reference implementation is tested against) exists because Oracle Labs needed to analyze codebases far too large for hand-written analyzers. An entire corner of smart-contract security stands on the same footing: the Gigahorse decompiler and the MadMax gas-vulnerability analyzer — the toolchain behind Dedaub’s audit platform — are Soufflé Datalog programs deriving facts about Ethereum bytecode. Program analysis turned out to be the paradigm’s beachhead for a simple reason: the input is a huge graph of facts, the questions are recursive, and being wrong quietly is expensive. Remember those three properties; they will recur.

You deployed to Kubernetes

If your cluster gates deployments through an admission controller, odds are the gate is written in Rego, the policy language of Open Policy Agent — a CNCF-graduated project whose documentation says plainly that the language “was inspired by Datalog.” A Rego policy is a set of rules deriving judgments (“this pod is non-compliant”) from facts (the pod spec, the registry allowlist, the namespace labels). No loops, no mutation; conditions in, conclusions out. Amazon went further along the same road with Cedar, its authorization-policy language: not only declarative but formally modeled — the language’s semantics lives as a machine-checked model in a proof assistant, and the production engine is battered against that model with millions of differential tests. Hold that design next to this book’s chapter 9: a small declarative language, a mathematical semantics, and mechanical checking of an untrusted implementation against it. Authorization converged on that architecture for the same reason compliance will: when the question is “who may do what,” you need the rule you enforce to be provably the rule you wrote.

You queried one, painfully

The fragment nearest to you is hiding in your database. WITH RECURSIVE — in the SQL standard since 1999, supported by Postgres, MySQL, SQLite, and everything else you run — is a fixpoint over rules: precisely the fragment of Datalog where recursion stays linear. Every org-chart rollup, bill-of-materials explosion, and dependency walk you have expressed in it was a logic program wearing SQL’s clothes, and you have felt the clothes chafe: the syntax fights recursion so hard that most teams write the query once, wrap it in a view, comment it “here be dragons”, and never touch it again. The lesson of WITH RECURSIVE cuts both ways: demand for recursive rules over relations is so real that the most conservative language committee in software shipped it — and ergonomics matter so much that shipping it in hostile syntax produced a feature everyone needs and no one loves.

Datomic took the opposite path: instead of bolting a fixpoint onto SQL it put a Datalog query language at the center of the database. That design has run a real bank — Nubank, whose core systems sit on Datomic at hundred-million-customer scale, liked the technology enough to buy the company that made it. One honest nuance, because this book promised precision: the newest system in that family, XTDB, made SQL its primary language in version 2, keeping only a Datalog-inspired secondary interface. Datalog-as-query-language remains a minority taste. The fixpoint is what proved indispensable; the surface syntax is still contested ground — a distinction this book will lean on hard when Strata-K has to choose its own surface.

And the commercial story has a second act that reads almost like this book’s thesis filed as a business plan. LogicBlox — the Datalog platform whose retail-forecasting deployments chapter 2 mentioned — was absorbed through two acquisitions into a larger vendor’s suite, the usual quiet end for a fragment. Except its founder started again: RelationalAI, built by the same lineage of people, ships a Datalog-family language as a “knowledge coprocessor” that runs inside Snowflake — inside the data warehouse the enterprise already has, next to the data it already trusts, funded to nine figures. Whatever comes of the company, note the shape of the bet, because it is a working businessman’s restatement of chapter 2’s third bet: don’t ask the industry to adopt a logic platform; bring the rules engine to the infrastructure that’s already paid for.

Fragments that worked, and one that didn’t survive

The pattern repeats wherever rules outweigh process. Three more data points, chosen because each carries a lesson forward.

Networks. VMware built DDlog — an incremental Datalog, where changed inputs update conclusions without recomputation — and used it to reimplement the brain of the OVN virtual-network controller: six thousand lines of rules deriving flow tables from network intent, recomputing in milliseconds what full evaluation took minutes to do. It worked. And the project is nonetheless archived today, unmaintained — not because the approach failed, but because a lone language with one corporate sponsor and one flagship deployment has no ecosystem to catch it when the sponsor’s priorities move. Fragments are fragile. Remember DDlog when this book argues that the pieces need to live in one language with one community; incrementality itself returns in chapter 5 as a load-bearing requirement.

Scheduling. The stable-models branch — ASP, the theory born in the winter — earns industrial money solving allocation problems: the port of Gioia Tauro assembles its container-terminal work teams with an ASP system; Swiss Federal Railways has run train-scheduling research on clingo with real timetables; a decision system built on ASP advised Space Shuttle flight controllers on reaction-control-system failures. Niche deployments, honestly counted — but note which niche: combinatorial choice under hard constraints, exactly the ground chapter 8 builds @asp on, and exactly where imperative code is at its most miserable.

Your own toolchain. The compiler whose type inference you rely on is a logic program you invoke a hundred times a day. “The type of f(x) is whatever f returns, provided x’s type matches what f accepts” — that is a rule, with variables, and inferring your program’s types means deriving the consequences of thousands of such rules until nothing new follows: a fixpoint, with unification doing the matching. When your IDE red-underlines a line and names the mismatch, you are reading the output of derivation, not of execution — and the reason type errors can be trusted (“if it compiles, the types hold everywhere”) is exactly the theorem-not-observation property chapter 6 will make Strata-K’s foundation. The build system completes the pair: make and its descendants compute which targets follow from which changed files — a fixpoint over dependency rules, so literally that make-in-Datalog is a standard classroom exercise. You have trusted logic programming with your builds and your types for your entire career. You just never had to call it that.

The shape of the evidence

Line the fragments up and read what they agree on.

Every fragment lives where three properties coincide: the domain is rule-shaped (policies, vulnerabilities, schedules, dependencies — knowledge, not procedure); wrong answers are expensive (security, money, law, broken builds); and the data is relational and recursive (graphs of calls, flows, ownership, dependency). That is the paradigm’s natural habitat, confirmed independently by security teams, database designers, network engineers, and logisticians who mostly don’t know the others exist. Note what the habitat is not: it is not “artificial intelligence.” The winter buried logic-programming-as-AI; the survivors are logic-programming-as-infrastructure, and none of them advertises the paradigm — the camouflage chapter 2 promised to explain. “Policy language,” “query language,” “code scanning,” “build tool”: the idea sells precisely when nobody says its name. A paradigm at once this useful and this unspeakable is a paradigm with a language problem, not an idea problem.

And the fragments do not add up. Each one solved the slice its niche demanded and stopped: CodeQL has world-class recursive queries and no notion of uncertainty; OPA decides but does not explain its decisions as derivations; WITH RECURSIVE has the fixpoint and syntax nobody defends; DDlog had incrementality and died of ecosystem; the ASP systems own hard choice and give yes/no answers only; none of them touches probability, cost, or learned components, though every one of their domains is full of all three — risk scores on vulnerabilities, confidence on policy inputs, weights on schedules. The engine survived everywhere. The language — one coherent tongue in which rules, recursion, choice, cost, probability, and explanation are citizens of the same semantics — survived nowhere. The fragments are a scattered proof of demand for it.

So the state of the field is this: an idea proven in production a dozen separate times, by a dozen communities, under a dozen names, with no common language to compound the wins. The obvious question — why not just crown one of the existing logic languages and consolidate? — deserves a serious answer, because the candidates are real: Prolog is alive and standardized, ASP has industrial solvers, CP is unmatched in its niche. The serious answer is chapter 4, and it requires a scalpel.

Chapter 4 — Autopsies

Chapter 2 told you how the paradigm rose and fell; chapter 3 showed its fragments thriving under assumed names. This chapter answers the question those two leave hanging: if the idea is this good, why did the languages built on it stall? Not the strawman versions — the real ones, each of which got something profoundly right and each of which hit a wall.

I’ll hold every system to the same three-part examination: what it got right, what limited it, and what a successor should inherit. And I’ll grade the limits against three axes that didn’t exist when these systems were designed, and that now decide everything:

• Hardware. Does the execution model parallelize? Modern performance is parallelism; a fundamentally sequential model has quietly lost the next thirty years.
• Machine generation. If an LLM writes programs in this language, do small mistakes stay small? Is meaning stable under reordering? Is a wrong program rejected with a reason, or does it silently misbehave?
• Expressiveness under guarantee. What can you say while keeping termination, determinism, and explainability — the properties that justified leaving your imperative language in the first place?

Each autopsy comes with a counterexample you can run. They live in examples/book/ch04/; the numbers below are from my machine, and the README there tells you how to reproduce them.

Prolog: the search procedure ate the logic

What it got right. Almost everything this book has praised so far, Prolog said first, and said beautifully: program as knowledge, rules you can read aloud, one language for data and logic. Fifty years of imitators — including this one — stand on it. It also proved the idea could be fast for its era: Warren’s abstract machine made a logic language compile to something competitive, on 1980s hardware, with 1980s memory.

What limited it. Prolog answers queries by a specific search procedure: try clauses top to bottom, try goals left to right, backtrack on failure. That procedure is the language’s soul and its wound, because it makes the order of your source code part of your program’s meaning. Here are the same three clauses from chapter 1, in Prolog, twice:

% path_good.pl                      % path_bad.pl — same clauses, reordered
path(X,Y) :- edge(X,Y).             path(X,Z) :- path(X,Y), edge(Y,Z).
path(X,Z) :- edge(X,Y), path(Y,Z).  path(X,Y) :- edge(X,Y).

Logically these are identical — the same two sentences, in a different order on the page. The first answers path(a,d) instantly. The second recurses into path before it has consulted a single fact, forever:

$ swipl -g "..." path_good.pl      → yes
$ timeout 10 swipl -g "..." path_bad.pl   → killed after 10 s, no answer

Not a wrong answer — no answer, no error, no diagnostic. A logically correct program that hangs because two lines swapped places. Every Prolog programmer learns to write clauses in the magic order, which is another way of saying every Prolog programmer learns to hand-compile the control flow after all — the thing the paradigm promised to take away. And when the magic order isn’t enough, Prolog offers the cut (!), an operator whose entire purpose is to reach into the search procedure and prune it. Cut is genuinely necessary in practice, and using it means your “declarative” program can no longer be read as sentences: it must be read as a trace.

Grade it against the axes. Hardware: depth-first backtracking is a fundamentally sequential walk of a proof tree; decades of parallel-Prolog research (and, as chapter 2 recounted, a Japanese national project) broke against it. Machine generation: meaning-depends-on-order is close to the worst property a generation target can have — an LLM that emits correct clauses in an unlucky arrangement produces a hang, the one failure mode that gives no error message to iterate on. Expressiveness: unbounded terms make Prolog Turing-complete, which sounds like a compliment but bills the programmer for it: termination is your problem, on every program, forever.

What a successor inherits. The dream itself — and the discipline to give it up per feature: Datalog is what remains of Prolog when you remove the things that made order matter. No term construction, no cut, no clause order, no goal order. Chapter 1’s engine finds the fixpoint in any order because there is nothing in the language that can observe the order. Prolog’s lesson is that the logic and the search must never share a syntax.

Expert-system shells: rules without a referee

What it got right. The 1980s shells — OPS5, ART, CLIPS, and their enterprise descendants like Drools — made two moves the industry still hasn’t fully absorbed. First: business rules deserve to live outside the application code, in a form domain experts can read — that’s the sanctions smear from the prologue, diagnosed correctly, in 1985. Second, a technical gem: the Rete algorithm, which matches thousands of rules against changing facts incrementally, reusing partial matches instead of re-evaluating from scratch. Squint and you’ll see the delta-driven evaluation from chapter 1’s engine; the lineage of that trick runs straight through this book to its GPU chapters.

What limited it. I speak from the inside here: I rebuilt one of these engines, and the rebuilding is how I learned where the crack runs. It isn’t in the matching — that part is brilliant. It’s in what happens after the match. When several rules match at once, a shell consults a conflict-resolution strategy to pick which fires first — and CLIPS ships seven of them (depth, breadth, simplicity, complexity, LEX, MEA, random). Switch strategy, and the same rules on the same facts can fire in a different order; and since a rule’s action can be any side effect — retract a fact, mutate a value, call out — a different firing order is, in general, a different final state. Read that back slowly: the rulebook alone does not determine the outcome; the rulebook plus a scheduling policy does. There is no fixpoint to trust, no model to check, no answer to the question “what do these rules, as such, entail?” A shell is not a declarative system; it is an event-driven imperative system whose statements look like rules.

The older cousins added a subtler warning about improvised mathematics. MYCIN — the 1970s medical expert system this whole product category descends from — attached “certainty factors” to its rules and combined them with ad-hoc formulas; researchers later showed the scheme is only coherent as probability under independence assumptions the rule base never satisfied. Numbers flowed through it and produced confident nonsense at scale. Chapter 7 will be this book’s answer to that story: if you attach numbers to inference, the arithmetic of combining them is the entire game, and it cannot be improvised.

Axes, briefly: hardware — Rete parallelizes moderately, but the strategy-then-side-effect loop at the core is inherently serial; generation — an LLM-written rule can be individually plausible and collectively catastrophic, with no compiler able to object, since almost nothing is statically wrong; expressiveness — unbounded, and therefore unanalyzable.

What a successor inherits. Rules outside code: right. Incremental delta matching: right, and generalized. And one hard-won principle, stated as a negative — no referee. In Strata-K there is no agenda and no strategy; all rules “fire” mathematically simultaneously into a fixpoint, side effects don’t exist, and two derivations of the same fact are one fact. What the shells needed was not a better conflict-resolution strategy but a semantics in which conflicts of that kind cannot arise.

ASP: the right semantics behind two walls

What it got right. Answer Set Programming fixed the exact disease of the previous two patients. A stable model (chapter 8 will make friends with the definition) is a property of the program — which sets of conclusions are self-consistent — with no reference to any evaluation order, strategy, or procedure. Modern solvers like clingo are engineering triumphs, and the modeling experience is the paradigm at its most honest: state what a valid schedule is, not how to search for one. It has real industrial deployments — chapter 3 visited the seaport.

What limited it. Two walls, one at each end of the pipeline. The entry wall is grounding: before solving, every rule is instantiated with every applicable combination of constants. A rule with three variables over a domain of size n grounds to n³ instances. Here is a two-line program, measured:

node(1..N).
triple(X,Y,Z) :- node(X), node(Y), node(Z).

N = 10   →      1,010 ground rules
N = 50   →    125,050
N = 200  →  8,000,200   (7.5 s just to ground, before any solving)

Two hundred of anything is not big data — it’s a small watchlist — and we’re already holding eight million instantiations. Real encodings are cleverer, and real grounders are excellent; but the cliff is structural, every serious ASP practitioner spends real effort “grounding-aware modeling,” and that phrase should sound familiar: it’s the magic clause order again, one abstraction level up. The exit wall is expressiveness of the answer: a stable model is a set of atoms — yes/no, all the way down. The moment your problem says “usually”, “how likely”, or “at what cost” (weak constraints handle simple cost, nothing native handles likelihood), you are outside the language. And between the walls sits a solver whose core search — conflict-driven, learning, sequential — is precisely the kind of algorithm GPUs are worst at.

Generation axis, worth its own paragraph: ASP semantics is global. Adding one innocent-looking rule can extinguish every stable model of the program, and the solver’s entire answer is UNSATISFIABLE — one word, no location, no witness. For a human expert this is a puzzle; for an LLM iterating on feedback it is a brick wall. Compare what a generation loop needs: local errors, with positions, with reasons.

What a successor inherits. The semantics itself — stable models are the correct meaning of unrestricted negation and choice, full stop. What changes is the placement: in Strata-K, ASP is an explicitly marked layer (@asp) you opt into for the subproblems that need choice, not the default cost of every program; the deductive core keeps its cheap, local, stratified world. The walls get attacked separately — grounding is a massively parallel enumeration (a GPU job, chapter 10), and the yes/no answer wall falls to the semiring machinery of chapter 7, which gives the deductive layer the “how likely / at what cost” vocabulary ASP never had.

Constraint programming: the model that lies about its price

What it got right. CP begins from an insight this book fully endorses: constraints are knowledge. “These two meetings can’t overlap” is a fact about the world, and propagating consequences of such facts — shrinking possibilities until only solutions remain — is inference, done by remarkably sophisticated engines. For scheduling, rostering, and configuration, CP solvers remain, to this day, some of the most effective tools humanity owns. Its cousin CHR distilled the idea to a beautiful minimum: computation as rewriting a store of constraints.

What limited it. The price of a CP model is invisible in its text. Here is the classic N-queens model in SWI-Prolog’s constraint library, N = 26 — one model, two runs, the only difference being the labeling annotation that tunes search order:

labeling([],  Qs)   →  8.019 s
labeling([ff], Qs)  →  0.014 s        # ~570× — same constraints, same solutions

Five hundred seventy times, from a hint that has no logical content whatsoever — both runs solve the identical problem and return valid boards. And it cuts both ways: an equally innocent change to the model (one extra constraint, one symmetry left unbroken) can take a solve from milliseconds past your deadline, with nothing in the source marking the cliff edge. CP experts earn their living knowing where the cliffs are. That expertise is real, and it is exactly the hand-compilation tax again: the what is declarative; the how leaks back in through heuristics, and the heuristics decide whether you get an answer today.

Axes. Hardware: propagation is a fine-grained, dependency-riddled fixpoint plus sequential search — decades of parallel-CP work, persistently modest speedups. Generation: the worst case on this axis isn’t wrong output, it’s plausible output — an LLM produces a perfectly correct model that happens to be 570× too slow, and no type checker, linter, or test on small inputs will catch it. Expressiveness: within its combinatorial niche, superb; as a general substrate, narrow.

What a successor inherits. Two design rules, both already constitutional in Strata-K. First: performance must be legible — every language construct has a documented cost in the execution model, and anything with a hidden exponential inside must wear a syntactic marker (you will meet this in chapter 7: the expensive question is spelled ?prob, and it looks expensive). Second: hints must be sterile — anything tunable may change the order of work, never the answer. The labeling flag actually honors that rule, and it’s the right kind of knob; the failure is that the knob is load-bearing and unmarked. Declare the cliff in the language, or the language is lying.

The matrix

Four autopsies, three axes, one table:

Read the table by columns and you can almost see the next language assembling itself. Column one demands an execution model that is parallel by construction — a fixpoint over sets, not a walk of a tree. Column two demands order-independence, locality of errors, and cost you can see in the source. Column three demands guarantees as the default and every escape hatch explicitly marked. None of the four patients died of a foolish idea; each died of one load-bearing coupling — logic to search, rules to scheduler, semantics to grounder, model to heuristic.

The next chapter turns this table upside down: it visits the systems being built right now, at the frontier, that each solve one column brilliantly — and shows that the puzzle piece missing is the language where the columns meet.

Run the autopsies. All four counterexamples, with exact commands and my measured numbers: examples/book/ch04/.

Chapter 5 — Converging Lines

The autopsies established why none of the classical languages can be the consolidation point. This chapter surveys what is being built right now — the research frontier of the last decade — because the frontier is where the missing pieces are being cut, one at a time, each by a community that needs that piece and no other. Six lines of work, converging; hold the ch. 4 matrix in mind as they pass, and watch each line fill a cell. Then we’ll write down, explicitly, the requirements they add up to — the specification the rest of this book tries to meet.

Line one: numbers on rules, done honestly

Chapter 7’s “a probability is not a weight” lesson was not news to researchers — the probabilistic logic programming community has owned it since Sato’s distribution semantics (1995) and ProbLog (2007): probabilities on facts, meaning defined over possible worlds, inference through compiled circuits rather than naive in-flight arithmetic — because in-flight arithmetic double-counts, exactly as you saw. The theory underneath is beautiful and general: provenance semirings (2007) showed that boolean truth, counting, weights, and full derivation-tracking are all the same computation with the arithmetic swapped out — one framework, one theorem, many meanings. That result is the mathematical spine of Strata-K’s chapter 7, and this book’s debt to it is total. What the probabilistic-logic line never had was an execution story fast enough to leave the lab at industrial data sizes. The pieces it cut: semiring parametrization, distribution semantics, circuit-based exact inference.

Line two: the neural boundary

DeepProbLog (2018) put neural networks inside a probabilistic logic program as predicates — the network estimates fact probabilities, the logic reasons over them, gradients flow back through the reasoning into the network’s weights. Exact and principled, but exact inference pays the circuit-compilation bill on every training step, which caps it at small problems. Scallop (2021–2023) made the engineering breakthrough: keep only the k most significant derivations per fact — top-k proofs, a deliberately declared approximation — and the whole pipeline becomes cheap enough to train real perception-plus-reasoning systems, while the semiring framework keeps the semantics honest about what was dropped. I want to be explicit here, because this is the closest living relative of the language in Part II: Strata-K borrows Scallop’s differentiable top-k-proofs idea directly for its own recursive-probabilistic layer, and says so. The differences — a GPU-first relational core rather than a Python-embedded interpreter, semirings surfaced in the language’s type system, an ASP layer, and a design aimed at LLM generation rather than perception pipelines — are differences of destination, not a dispute about this piece. (The Scallop group itself is now building GPU-accelerated successors — Lobster, 2025 — which should tell you which way the wind blows.) Pieces cut: neural predicates at the boundary, declared top-k approximation, gradients through logic.

Line three: don’t recompute the world

Differential dataflow — Frank McSherry’s line of work, now the engine inside the Materialize streaming database — solved incremental maintenance in full generality: arbitrarily nested recursive computations whose outputs update in milliseconds when inputs change, without recomputation. DDlog (chapter 3’s fallen fragment) was exactly this piece bolted to Datalog, and its OVN deployment proved the fit before the project was orphaned. For the trading-house world this piece is not optional garnish: facts arrive as a stream — trades, quotes, ownership updates — and an engine that re-derives the world per tick is a toy. Strata-K’s phase for this is explicitly on the roadmap and explicitly not built; the piece exists, proven, in the literature. Piece cut: incremental fixpoints.

Line four: equalities, solvers, and other engines bolted on

Two shorter lines, same moral. The egg/egglog line (2021–2023) unified Datalog with equality saturation — rule-driven discovery of “these expressions are equal” — and jumped from a POPL paper into the guts of a production compiler backend (Cranelift’s e-graph mid-end) in about two years, the fastest lab-to-production transfer in this survey; rewriting-modulo-equality turns out to be what an optimizer is. Formulog (2020) welded SMT-solver calls into Datalog rules so that static analyses can derive facts and discharge logical side-conditions in one program. Neither piece is on Strata-K’s v1 roadmap, and honesty is cheap here: these lines prove the shape — a fixpoint rule core with a specialized engine grafted on at marked points — which is precisely the shape Strata-K uses for its own grafts (@asp, ?prob, neural). Pieces cut: the graft architecture, and proof that it ships.

Line five: the model writes, the solver checks

The last line is the youngest and the one this book bets on. Since 2023, a rapid research thread — Logic-LM, LINC, and successors — has converged on one workflow: the LLM translates a natural-language problem into a formal program; a symbolic engine (SAT, SMT, a prover, an ASP solver) does the reasoning; errors from the engine loop back to the model for repair. The gains over “let the LLM reason in prose” are large and reproduced. IRIS (2025) runs the pattern at industrial scale — LLM-inferred specifications feeding CodeQL for vulnerability detection. And a 2025 thread with a title I could have used for this book — “Intermediate Languages Matter” — measures the point directly: which formal language the LLM targets materially changes end-to-end accuracy. The target language is a design variable. No one has yet built the language designed as that target — the entry in the design space optimized for machine writability, checkability, and explanation rather than human writability. That is the empty seat Strata-K is aimed at, and chapter 9 is the audition. Piece cut: the propose–verify loop, validated; the purpose-built target, missing.

Line six: the hardware finally answers

And the piece FGCS died waiting for: GPU Datalog is now real research. GDlog (2023–2025) showed hash-indexed semi-naive evaluation running whole program analyses on GPUs, with the fixpoint’s inherent parallelism finally cashed as wall-clock time; column-oriented successors (2025) then beat it with exactly the storage layout a GPU wants. These are early systems — research-grade, benchmark-oriented, none yet carrying semirings or probability — but the existence proof is banked, and its shape is worth savoring: the branch of logic programming that the winter’s flagship project passed over is the one now riding the hardware that deep learning paid for. Chapter 2’s third bet, already being placed by others. Strata-K’s GPU engine — designed, unbuilt, chapter 10 — enters a race that has visibly started, which is both validation and pressure. Piece cut: the existence proof.

What Strata-K is not trying to be

Before assembling the requirements, the disclaimers that keep them honest. Strata-K is not a theorem prover — no quantifiers over infinite domains, no induction, no proof search; Lean and Isabelle own that ground. Not constraint programming over continuous domains — schedule optimization over reals stays with CP/MILP solvers, which are superb. Not a neural framework — it will never train a network; it consumes their outputs at a typed boundary and hands gradients back. Not a general-purpose language — chapter 1 already made that trade, and this book will not un-make it. Every one of these refusals buys guarantees inside the fence; the fence is the product.

The requirements

Time to collect. Six lines of frontier work, four autopsies, a chapter of fragments in production — everything this half of the book has established compresses into a specification. I’ll state it as six requirements. None of them is my invention; each is the direct print of a wall someone hit, and I’ll name the wall each time. Together they describe a language that, as of this writing, does not exist.

One: parallel by construction. The core execution model must be a fixpoint over sets of facts — work that exists in bulk, all of it independent within a pass — and never a search through a tree whose meaning is welded to the order of traversal. This is the difference you watched in chapter 4 between the engine that shrugged off clause reordering and the one that hung: not an implementation detail but the dividing line between a paradigm that can ride parallel hardware and one that structurally cannot. Prolog stood on the wrong side of the line; FGCS spent a national budget learning how much that matters; line six above shows the right side finally being cashed in. A language designed today has no excuse for standing anywhere else.

Two: meaning independent of order, errors local and named. Reorder the rules, the facts, the files — the answer must not move. And when a program is wrong, the language must say where and why: a position, a reason, ideally a fix. Never Prolog’s silent hang; never ASP’s bare UNSATISFIABLE with no witness. In the era chapter 2 ended on, this requirement stops being ergonomics and becomes infrastructure: a generation loop — model writes, checker responds, model repairs — is only as good as the error messages that drive it. A language whose failure modes are silence and global mystery starves the loop; a language whose failures are local and named feeds it.

Three: guarantees by default, escapes marked. The core must terminate, always, and mean one thing, always — chapter 1’s bargain, kept with no exceptions. Everything that weakens a guarantee — unrestricted negation and choice, probability, a neural network’s opinion — must be a visible, syntactic opt-in, a fence the reader can see. The expert shells taught the cost of the alternative: power mixed invisibly into the semantics until no one could say what the rulebook, as such, entailed. The frontier’s graft architecture (line four) shows the same principle succeeding: a clean core, with specialized engines attached at marked points.

Four: pluggable arithmetic, honestly divided. One rule language, many meanings — boolean, cost, probability — by swapping the arithmetic, exactly as the provenance-semiring theory (line one) promises and as chapter 7 demonstrated. But the demonstration came with a scar: some arithmetics tolerate the fixpoint’s repetitions and some are corrupted by them, and the boundary must be enforced by the language, not documented in a footnote for the user to trip over. MYCIN improvised its arithmetic and produced confident nonsense; ASP refused numbers entirely and hit the boolean wall. The requirement is the narrow path between: numbers on rules, with the double-counting line drawn in the type system.

Five: cost legible in the source. Reading a program must reveal what is cheap, what is expensive, and what is approximate. The CP autopsy is the cautionary tale — a 570× cliff invisible in the model’s text — and the requirement generalizes it: expensive questions should look expensive (the ?prob principle), approximations should be declared where they’re ordered, and no annotation that claims to be a mere hint may ever change an answer. This one matters double under machine generation, because an LLM inherits only the costs it can see; a language that hides its cliffs will have them found at 3 a.m., in production, by the one reader who never sleeps but also never profiles.

Six: explanation as a native object. Every derived fact must be able to produce its derivation — its pedigree, as chapter 1 called it — as a first-class value, not a debug log. Twice over, this book has argued, the future demands it: once for the auditor, who in a regulated industry is entitled to “why was this trade blocked?” as a matter of law; and once for the verification loop of line five, where a human confronted with machine-written rules needs the system itself to unfold what those rules concluded and from what. Explanation is the one requirement the fragments of chapter 3 missed almost universally — and the one that gives this book its title.

Read the list once more, and notice two things about it. Nothing on it is exotic — every requirement is already met, in isolation, by some system named in this chapter or the last. And nothing currently meets more than three of the six at once. The pieces exist, cut and polished by communities that rarely cite one another. What’s missing is the table they assemble on.

Part II is my attempt to build that table. It starts small — a trading house, some facts, two rules — and it starts the way chapter 4 taught me all such attempts should start: with an honest status box.

Chapter 6 — Meet Strata-K

Status — read this first. Everything you run in chapters 6 through 9 executes today, on the CPU reference implementation in the book’s repository: parser, type checker, evaluator, exact probabilistic queries, answer-set solver — cross-checked against the independent Soufflé engine on the shared fragment, and fuzzed against itself over tens of thousands of random programs. What does not exist yet: the GPU engine (chapter 10 — design, no benchmarks), the neural boundary and the scaled probabilistic machinery (chapter 11 — vision, marked as such). Code shown inside a “future syntax” frame parses today and executes in a later phase; everything else runs, and every output printed in this book is the tool’s real output. That’s the deal, and it holds to the last page.

Part I ended with six requirements and an empty table. Time to put something on it — not the whole language at once, but its deductive core, on a worked example sized like the real world’s problems and small enough to hold in your head. This chapter’s job is for you to read a complete Strata-K program the way its checker does, and to see the first three requirements — parallel-ready core, order-independence, guarantees by default — fall out of decisions you can point at in the source.

The trading house

Meet the world every remaining chapter builds on. A trading house faces a web of counterparties — firms it buys from, sells to, clears through. Firms own stakes in other firms. A regulator publishes a sanctions list. And the rule from the prologue applies in its full inconvenience: a counterparty is untouchable if anyone who ultimately controls it is listed.

Here is the entire compliance kernel, as a program — examples/book/ch06-trading-house.strata:

domain firm.

pred owns(firm, firm): Bool.        % direct ownership stakes
pred controls(firm, firm): Bool.    % beneficial control, any depth
pred listed(firm): Bool.            % appears on the sanctions list
pred counterparty(firm): Bool.      % firms we actually trade with
pred blocked(firm): Bool.           % barred by the sanctions rule
pred cleared(firm): Bool.           % free to trade
pred stake_count(firm, int): Bool.  % how many direct stakes a firm holds

% The regulation, as rules.
controls(X, Y) :- owns(X, Y).
controls(X, Z) :- owns(X, Y), controls(Y, Z).

blocked(C) :- counterparty(C), listed(C).
blocked(C) :- counterparty(C), controls(P, C), listed(P).

cleared(C) :- counterparty(C), not blocked(C).

stake_count(X, count<Y>) :- owns(X, Y).

% The world as we know it today.
owns(apex, brightwater).
owns(apex, cobalt).
owns(brightwater, dunlin).
owns(cobalt, eiders).
owns(fenwick, gullwing).

listed(apex).

counterparty(dunlin).
counterparty(eiders).
counterparty(gullwing).

Thirty-odd lines, three sections — declarations, rules, facts — and you have already met most of the ideas in Part I. Let’s read it top to bottom, stopping wherever a design decision is doing work.

Declarations: the part Datalog never had

The block of pred lines is the first thing a Datalog veteran would notice, because classical Datalog doesn’t have it: every predicate must be declared, with the domains of its arguments and an annotation after the colon. Bool says these are plain true-or-false facts — the only annotation this chapter needs; the next chapter is entirely about what else can stand in that position.

Design note — why signatures are mandatory. In classical Datalog, Prolog, and every expert shell, referring to a predicate that doesn’t exist is not an error — it is simply a predicate with no facts, silently true nowhere. Misspell listed in a rule and the rule quietly never fires; your sanctions check runs, passes every test that doesn’t cover the typo, and clears everything. In a language meant to be written at speed by machines and reviewed by busy humans, that failure mode is disqualifying. Strata-K closes it structurally: every predicate is declared, so a misspelling is a compile error with a location, not an empty relation. You will watch this exact scenario play out, with real tool output, in chapter 9 — it is requirement two of chapter 5, cashed in.

The declarations also carry the types. owns(firm, firm) relates firms to firms; stake_count(firm, int) pairs a firm with a number. Arities and argument types are checked everywhere the predicate appears — one more class of silent nonsense (swapped arguments, wrong arity) converted into named, located errors.

Rules: the regulation, executable

The rules section you can already read fluently. controls is chapter 1’s transitive closure, verbatim. The two blocked rules are the regulation’s two cases — directly listed, or controlled at any depth by someone listed — and note that they are two separate rules, not one rule with an or: in this language, alternatives are alternative rules. Multiple rules for the same head are how disjunction is spelled, and the engine treats every derivation route identically — you saw in chapter 1 why duplicate derivations cost nothing here.

cleared introduces the one genuinely new construct of this chapter, and it deserves its own section.

Negation, stratified: computing what’s absent

cleared(C) :- counterparty(C), not blocked(C).

Read it aloud: C is cleared if C is a counterparty and C is not blocked. Nothing looks dangerous. But not in a fixpoint language is a genuinely subtle guest, and the subtlety is worth two minutes, because the language’s answer to it is one of its load-bearing walls.

The fixpoint of chapter 1 grows monotonically: every pass adds facts, and nothing ever becomes false again. not blocked(C) breaks that comfort — it asks about the absence of a fact. Absence when? If the engine checks “is blocked(dunlin) absent?” too early — before the blocked rules have finished firing — it might conclude cleared(dunlin), then later derive blocked(dunlin), and now the model contradicts itself. Worse, feed negation back into its own definition — p :- not p. — and there is no sensible answer at all: if p is false it must be true, if true it must be false. The liar’s paradox, in one line.

Strata-K’s rule is the classical one, and it is exactly the plain-English sentence from this book’s glossary: you may only negate what has been fully computed first. The checker builds the dependency graph of predicates and splits the program into strata — layers. owns, listed, counterparty sit at the bottom; controls and blocked build on them; cleared, which negates blocked, sits in a stratum strictly above it. The engine runs each stratum to its fixpoint before the next begins, so by the time any rule asks not blocked(C), the set of blocked firms is finished and frozen — the question has one answer, forever. And a program whose negation can’t be layered — any cycle through a not, with the liar as the smallest case — is rejected at compile time, with the offending predicate named in the error.

Pause on the shape of that guarantee, because it is the constitution of this language in miniature (you met the idea as a refrain starting in chapter 5): a fact derived in this program is not “true as of when we checked, under the depth strategy, unless a later rule retracted it” — the hedges you’d wear in an expert shell. It is a theorem: a consequence of the stated facts and rules, unconditionally, reproducibly, in any evaluation order. The language’s first invariant says exactly this — nothing approximate may leak into a Bool derivation without a compile error — and each extension in the coming chapters will be measured against it.

There is one honest limitation to flag now: some problems want the unstratifiable shape — not as paradox but as choice, where “assume it’s in, unless it’s out” is the actual specification. The deductive core refuses those programs. Chapter 8 opens the fenced yard where they are welcome.

Aggregates, and running the world

stake_count(X, count<Y>) :- owns(X, Y). — for each X, count the Ys. The aggregate vocabulary is count, sum, min, max, and the same stratification logic governs it: aggregation, like negation, needs its input finished before it summarizes, so it lives between strata, never inside a recursive loop (one carve-out comes in the next chapter, where a particular aggregate and a particular arithmetic turn out to be made for each other).

Run the world:

$ strata run examples/book/ch06-trading-house.strata
blocked(dunlin)
blocked(eiders)
cleared(gullwing)
controls(apex, brightwater)
controls(apex, cobalt)
controls(apex, dunlin)
controls(apex, eiders)
...
stake_count(apex, 2)
stake_count(brightwater, 1)
stake_count(cobalt, 1)
stake_count(fenwick, 1)

Trace blocked(dunlin) yourself, once, on paper — it’s three steps and it is the whole paradigm: owns(apex, brightwater) and owns(brightwater, dunlin) give controls(apex, dunlin) through the recursion; listed(apex) plus counterparty(dunlin) fire the second blocked rule. Dunlin is untouchable because of who sits two levels above it, and nobody wrote the walk — no depth parameter, no cache, no nightly job. Eiders falls the same way through cobalt. Gullwing, owned by unlisted fenwick, clears. The prologue’s smear — recursive walk, flattening cache, depth limit, hotfix — is these thirty lines, and the depth limit that someone hard-coded as 3 out of fear is simply gone, because the fixpoint has no depth to limit.

And the compliance officer can read the rules. That sentence is easy to skim past, so let me weigh it: the artifact the engineers maintain and the artifact the domain expert can verify are, for the first time in this book, the same artifact.

What you can no longer write

A tour of this language is incomplete without the negative space — the imperative habits that have no translation here, each one a deliberate absence:

You cannot order anything. There is no “first this rule, then that one.” Rules fire logically simultaneously; files concatenate in any order; the answer is the fixpoint, full stop. The freedom you’re giving up was never freedom — it was the hand-compilation of control that Part I spent four chapters indicting.

You cannot update or delete. No rule retracts a fact. Within a run, the world only grows toward its fixpoint — that’s what makes derived facts theorems (and, later, what makes the engine massively parallel and the incremental story tractable). “The data changed” is handled where it belongs: new facts in, run again — and efficiently reusing the previous answer is the engine’s job on the roadmap, not a mutation you perform by hand.

You cannot call anything. No side effects, no I/O in rules, no escape into a host language from inside the logic. The expert shells’ original sin — rule bodies doing arbitrary things, meaning held hostage by firing order — is not restricted here; it is absent.

Each absence is a requirement from chapter 5 wearing work clothes. Determinism and order-independence aren’t features the implementation strives for; they are what’s left when the constructs that could violate them are removed from the grammar.

Try it.

cargo run -p strata-cli -- run examples/book/ch06-trading-house.strata

Then: (1) add owns(gullwing, fenwick). — a two-firm ownership cycle — and watch controls close over it harmlessly; (2) misspell listed as listd in a rule and run strata check on the file — chapter 9 will make this error message the hero of a longer story; (3) try the liar: add pred p(): Bool. and p() :- not p(). and read the stratification error.

One word of the signature — that Bool after the colon — has been sitting quietly through this whole chapter. The next chapter changes it, twice, and the second change breaks something important on purpose.

Chapter 7 — Change One Word

Phase-0 status: everything in this chapter runs today — Trop natively, ?prob by the exact reference method. The scaled probabilistic machinery is described where it differs; chapter 11 places it on the roadmap.

The trading house doesn’t only ask yes-or-no questions. The logistics desk doesn’t ask whether goods can move from Rotterdam to Tallinn — of course they can — it asks what the cheapest way is. The risk desk doesn’t ask whether trouble at Apex can reach Dunlin — chapter 6 answered that — it asks how likely it is. Same relations, same recursive structure, different arithmetic.

The imperative playbook at this point is grim: the boolean reachability code, the shortest-path code, and the risk-propagation code are three unrelated programs — Dijkstra’s algorithm shares no line with your graph walk — maintained by three people, drifting apart from the day they’re written. This chapter makes an unreasonable-sounding claim instead: they are one program. The difference between them is, almost literally, one word — and the “almost” is where the chapter’s real lesson lives.

Costs: the same rules, priced

Here is the logistics network — examples/book/ch07-routes.strata:

domain hub.

pred leg(hub, hub): Trop.     % direct transport legs, cost per unit
pred route(hub, hub): Trop.   % best achievable cost, any number of legs

route(X, Y) :- leg(X, Y).
route(X, Z) :- leg(X, Y), route(Y, Z).

4 :: leg(rotterdam, gdansk).
8 :: leg(rotterdam, riga).
3 :: leg(gdansk, riga).
5 :: leg(riga, tallinn).
9 :: leg(gdansk, tallinn).

Two changes from anything in chapter 6. The annotation in the signatures says Trop instead of Bool. And facts now carry a number: 4 :: leg(rotterdam, gdansk) — this leg exists at cost 4. The two rules defining route are chapter 1’s transitive closure, unmodified, character for character.

$ strata run examples/book/ch07-routes.strata
leg(rotterdam, gdansk) = 4
...
route(rotterdam, gdansk) = 4
route(rotterdam, riga) = 7
route(rotterdam, tallinn) = 12
route(gdansk, riga) = 3
route(gdansk, tallinn) = 8
route(riga, tallinn) = 5

Look at route(rotterdam, riga) = 7. There is a direct leg at cost 8 — and the engine reports 7, having noticed that going through Gdańsk (4 + 3) beats flying direct. route(rotterdam, tallinn) = 12 is the three-leg chain 4 + 3 + 5, beating both alternatives (13 either way). Nobody wrote Dijkstra. Nobody wrote anything — the rules didn’t change. What changed is what the engine does when derivations meet.

What the word actually switches

Under Bool, the fixpoint’s bookkeeping is: a chain of conditions is an and; multiple derivations of the same fact are an or; and the values are true/false. Under Trop — the name is tropical, a mathematician’s in-joke you can safely ignore — the bookkeeping is: along a chain, add the costs; when derivations meet, take the minimum. That pair of operations is the entire difference. Reachability and shortest-path were never two algorithms; they were one algorithm with two accounting policies:

A structure like this — values, a “combine along the way” operation, a “merge alternatives” operation, obeying a handful of sanity laws — is called a semiring, and it is the taught concept of this chapter, the “pluggable arithmetic of inference” promised since chapter 5. The rules define the shape of inference: which facts combine, which conclusions compete. The semiring defines what flows through that shape. One program, many meanings — this is requirement four from chapter 5 arriving in the language, and it is the direct, working descendant of the provenance-semiring theory chapter 5 credited.

Two footnotes with teeth, both enforced rather than advised. Convergence: the fixpoint under Trop still terminates, because min can only improve a finite number of times — but negative cost cycles would let a route improve forever, so cycle detection is the engine’s mandated job, not the user’s assumed discipline. And the aggregate carve-out promised in chapter 6: min in recursion is legal under Trop precisely because minimum is this semiring’s merge operation — the aggregate and the arithmetic are the same object, which is why that one aggregate escapes the between-strata rule.

If your suspicion is up — “swap the arithmetic, keep the engine” sounds too clean — good. It is too clean. One more word-swap and it breaks.

Probabilities: the same move fails

After a trick that clean, you can see the next move from here. Costs worked by swapping one word — surely probabilities are one more swap: multiply along the chain, or-combine where derivations meet. Every textbook formula is standing by.

Let’s walk into it with open eyes, on the risk desk’s actual question. Apex has a 50% chance of being exposed to Brightwater — a disputed guarantee, say, that stands or falls with one court ruling. From Brightwater, contagion has two onward routes to Dunlin: directly (75%), or through Cobalt (75%, then a certain link). What is the chance trouble at Apex reaches Dunlin?

The one-more-swap arithmetic says: multiply along each route — route one: 0.5 × 0.75 = 0.375; route two: 0.5 × 0.75 × 1.0 = 0.375 — then combine the two routes: 1 − (1 − 0.375)(1 − 0.375) = 0.609375.

Look at that number until it bothers you. Every route from Apex to Dunlin — both of them — crosses the same first link: the disputed guarantee, the one that exists with probability 0.5. If the court ruling goes the other way, there is no exposure at all, through anything. The chance of contagion reaching Dunlin cannot possibly exceed 0.5 — and we just computed 0.609 with textbook formulas and a straight face. This is not a rounding problem. The arithmetic answered a different question than the one we asked.

The bug has a name — double counting — and you have met it before, most likely in an availability review. Service A is 99.9% available, B is 99.9%, so A-or-B fails only when both do: 99.9999%! Except A and B run in the same rack, and the number evaporates with one power supply. The combining formula is honest only for independent witnesses, and our two contagion routes are not independent witnesses — they are one witness, the disputed guarantee, wearing two hats. Combining as the facts flow treats every route as fresh evidence; shared evidence gets counted once per route it appears in; every extra count inflates the answer.

Now the sharper question: why didn’t this bite us with costs? Routes shared links there too — and the answer was exactly right. Because min is immune by nature: consider the same route twice, or ten times, and the minimum doesn’t move. Counting duplicate evidence is free under an arithmetic that only keeps the best, and poison under an arithmetic that accumulates. That one word in the signature was doing more work than it seemed — and “does this arithmetic forgive repetition?” turns out to be the exact line between the numbers you may compute as the facts flow and the numbers you may not.

The two modes, and the marked question

Strata-K draws that line in the type system, and refuses to let you cross it silently.

Arithmetics that forgive repetition — Bool, Trop, and their relatives — ride inside the fixpoint: the value is one more column on the fact, updated on the fly. The engine calls this mode A, and everything before this section ran in it.

Probability is mode B, and mode B changes regime entirely: during the fixpoint the engine computes no probabilities at all. Instead it records, for every derived fact, its pedigree — the full structure of which base facts, combined by which rules, support it, shared evidence and all. Chapter 1 introduced that structure as provenance, the answer to “why was this trade blocked?”. Here provenance stops being documentation and becomes the computation itself: the pedigree of the queried fact is compiled into a circuit that counts each base fact exactly once, no matter how many derivations it appears in, and the probability falls out of the circuit, correct by construction.

You ask for it with a marked question — examples/book/ch07-shared-evidence.strata ends with one:

0.5 :: exposed(apex, brightwater).    % the shared link
0.75 :: exposed(brightwater, dunlin). % route 1
0.75 :: exposed(brightwater, cobalt). % route 2, first hop
exposed(cobalt, dunlin).              % route 2, certain hop

?prob hit(apex, dunlin).

$ strata run examples/book/ch07-shared-evidence.strata
0.46875 :: hit(apex, dunlin)

Below 0.5, as sanity demands: the court ruling gates everything, and behind the gate the two routes together deliver 0.9375. Half of that is the honest answer — the naive figure overstated it by nearly a quarter. Overstated contagion risk errs safe, this once; the same double-count sitting under a netting rule errs the other way. Pick which of your systems you’d rather have wrong.

Why mark the question as ?prob instead of just answering? Because the circuit is not free. For pedigrees that tangle badly, compiling one is genuinely, irreducibly expensive — this is the field where “how hard is it to count without double-counting” is a famous hard problem, and no engineering makes the worst case vanish. So the language keeps the CP autopsy’s promise, requirement five: cheap questions look cheap, expensive questions look expensive, and the expensive one is where you’ll attach a budget when the scaled engine arrives (chapter 11 shows the declared-approximation escape valve — top-k pedigrees, borrowed with attribution from Scallop — whose guarantee is honest: a lower bound that only tightens).

One more enforcement, easy to miss and deeply typical of this language: Trop and probability do not mix. There is no honest exchange rate between a cost and a likelihood — no formula turns “cost 7” into “70% likely” without you asserting one — so the language refuses the combination: ask ?prob of anything derived through a Trop predicate and the Phase-0 reference stops you with a named refusal at the query (the full type system, specified but not yet the enforcer, makes it a compile error at the rule site); when you want a conversion, you will write it as an explicit, named function that owns its assumptions. Where the mathematics has no bridge, the language refuses to paint one; every approximation and every conversion is declared, or it doesn’t happen. You have now seen the language’s second invariant in action twice; it will not be the last time.

The aggregate corollary

Chapter 6 left a promissory note in its aggregates section — count and sum live between strata, never inside a recursive loop, with one carve-out to be explained here. This chapter has quietly supplied everything the explanation needs, so let’s collect the debt; it takes three short experiments, two of which end in instructive refusals.

First experiment: count something across the arithmetic line. It seems innocent — “how many destinations can each hub reach?” — a Bool-flavored summary of a Trop-flavored relation:

pred options(hub, int): Bool.
options(X, count<Y>) :- route(X, Y).

error[E1007]: `route` (Trop) cannot flow into `options` (Bool); use an explicit conversion

The no-silent-crossing law you just met on the probability side turns out to guard every border between arithmetics, aggregation included — and this direction is refused for its own good reason: route facts carry costs, and “count them into a plain boolean world” silently discards the costs, which is a decision the language insists you make out loud. (Going the other way, recall, is free: Bool embeds into any arithmetic honestly, a fact at cost zero, a truth with probability one.)

Second experiment: let a count feed its own recursion — some “how many firms sit below X, counting transitively” formulation. The checker stops you with the same error code that rejected chapter 6’s liar paradox, and the kinship is not cosmetic:

error[E1002]: predicate `deep` depends on its own negation/aggregation through a cycle

Here is the deep reason, and it is this chapter’s lesson wearing a third costume. Ask why a self-feeding count is dangerous: the fixpoint re-derives facts freely — chapter 1 told you duplicate derivations are harmless — and a count that can see its own output counts its own repetitions. Sound familiar? Non-idempotent accumulation inside the fixpoint — the exact disease of the naive probability, wearing an integer instead of a fraction. min was immune, probabilities were poisoned, and sum/count are poisoned the same way. The language’s response is graded by severity, and the grading is the design: arithmetics that forgive repetition ride the fixpoint (mode A); those that don’t but have a sound alternative route go through the pedigree (mode B, ?prob); and those where v1 has no honest story — recursive counting among them — are refused outright, by name, at compile time, rather than shipped with a footnote. Three answers, one criterion, no improvisation.

Third experiment, the carve-out, and now it’s one sentence: min in recursion under Trop is legal because minimum is this semiring’s merge operation — the aggregate and the arithmetic are the same object, so “aggregate inside the loop” and “run the fixpoint” mean the same thing. What looked in chapter 6 like an arbitrary exception is the table at the top of this chapter, read back at you.

One program, priced three ways

Step back to the chapter’s unreasonable claim: reachability, cheapest route, contagion probability — one shape, three arithmetics, and the language now owes you nothing it hasn’t shown. The rules stayed fixed while the meaning moved: that’s the semiring dividend. The meaning that couldn’t move honestly was stopped at compile time: that’s the double-counting line. And the question that costs more than a lookup is spelled differently: that’s legibility of cost. The trading house has its logistics desk and its risk desk running on the compliance desk’s rules.

What it doesn’t have yet is a way to decide anything — every number so far describes the world as it is. The next chapter hands the language its first genuinely hard power: choosing.

Try it.

cargo run -p strata-cli -- run examples/book/ch07-routes.strata
cargo run -p strata-cli -- run examples/book/ch07-shared-evidence.strata

Then: (1) drop the Gdańsk–Riga leg to cost 2 and watch the improvement propagate through both downstream routes; (2) in the risk file, make the two onward routes share another link and check that the naive formula’s error grows while ?prob stays sane; (3) change 0.5 to 1.0 on the shared link and confirm the answer becomes exactly the two-route combination 0.9375.

Chapter 8 — Choices Under Constraints

Phase-0 status: everything here runs today, on the reference answer-set solver in the repository.

Everything the language has done so far — deriving, pricing, weighing — describes the world as it is. But half the interesting questions at a trading house are not “what follows?” but “what should we pick?” The portfolio desk holds a list of candidate positions and a book of mandates: certain pairs may not be held together — a client agreement forbids holding gas futures against carbon credits, say. Which combinations of positions are acceptable?

Feel how the ground shifts under that question. It has no single answer — there are many acceptable portfolios, and enumerating the legitimate alternatives is the deliverable. The deductive core of chapters 6 and 7 is constitutionally incapable of this, and proudly so: its whole guarantee is that the facts and rules determine one fixpoint, every derived fact a theorem. “Pick some subset, any consistent one” is not a theorem. Ask an imperative programmer and you get the third member of the zoo from chapter 1 — next to the graph walk and the worklist, there’s the backtracking enumerator with the pruning conditions threaded through it, the one whose recursion nobody wants to touch.

Chapter 4 already met the paradigm built for exactly this — ASP — and found the semantics right and the walls real. So Strata-K does the only honest thing: it takes the semantics and fences it. That fence is the pragma at the top of today’s file, and it is the language’s third invariant made visible: guarantees by default, escapes explicit and marked. Outside the fence, the deductive world of one-true-fixpoint. Inside, a different physics.

The program

examples/book/ch08-portfolio.strata:

@asp.
domain pos.

pred candidate(pos): Bool.
pred take(pos): Bool.
pred skip(pos): Bool.
pred conflict(pos, pos): Bool.
pred viol(): Bool.

% Each candidate position is independently taken or skipped.
take(P) :- candidate(P), not skip(P).
skip(P) :- candidate(P), not take(P).

% Mandates: these pairs may not be held together.
conflict(gas_futures, carbon_credits).
conflict(carbon_credits, gas_futures).

% No self-consistent world may hold a conflicting pair.
viol() :- take(X), take(Y), conflict(X, Y), not viol().

candidate(gas_futures).
candidate(carbon_credits).
candidate(fx_swap).

Stop at the pair of rules defining take and skip, because chapter 6 trained you to reject them on sight: take depends on the negation of skip, skip on the negation of take — a cycle through not, exactly what the stratification checker rejects programs for. Inside @asp, this shape is not an accident to be rejected; it is the idiom, and what it expresses is choice.

Stable models: self-consistent worlds

Here is the semantics, in the plain terms this book promised. A stable model is a set of conclusions that earns its keep in both directions: take the set as given — treat every not q in the rules as settled by whether q is in the set — and re-derive everything the rules then produce. If you get back exactly the set you assumed — nothing missing, nothing extra, every member re-derivable — the set is stable: a self-consistent world. If the assumption produces more than it assumed, or fails to reproduce a member, it was never a coherent world at all, just a wrong guess.

Run the take/skip pair through that definition for one candidate, fx_swap. Assume a world where take(fx_swap) holds and skip(fx_swap) doesn’t: then not skip(fx_swap) is settled-true, the first rule re-derives take(fx_swap), the second is blocked — the world reproduces itself exactly. Stable. The mirror-image world (skip, no take) is stable by symmetry. But a world with neither: both nots are settled-true, both rules fire, and the re-derivation produces both facts where zero were assumed — not a world, a contradiction. And a world with both fails the other direction: each rule is blocked by the other’s conclusion, nothing is re-derivable, yet the assumption claimed both. The two-rule cycle is therefore a fork with exactly two self-consistent resolutions per candidate — an “or” that the one-fixpoint core could never speak. Three independent candidates: 2 × 2 × 2 = eight candidate worlds.

The viol rule then kills the bad ones, and it works by weaponizing the liar’s paradox from chapter 6. Read it again: if a conflicting pair is held and viol() is not in the world, the rule derives viol() — the assumption fails to reproduce itself. If you instead assume viol() is in the world, the not viol() in its own body blocks the only rule that could derive it — and an underivable assumption is also unstable. Heads you lose, tails you lose: no stable world can hold a conflicting pair. The paradox that the deductive core rejects at compile time becomes, inside the fence, a scalpel for cutting worlds away. (I’ll be honest about ergonomics: production ASP dialects spell this pattern with dedicated constraint syntax rather than an explicit paradox loop, and surface sugar for it is on Strata-K’s roadmap — what you see here is the semantic mechanism itself, undisguised.)

$ strata run examples/book/ch08-portfolio.strata
Answer 1: {..., skip(carbon_credits), skip(fx_swap), skip(gas_futures)}
Answer 2: {..., skip(carbon_credits), skip(fx_swap), take(gas_futures)}
Answer 3: {..., skip(carbon_credits), skip(gas_futures), take(fx_swap)}
Answer 4: {..., skip(carbon_credits), take(fx_swap), take(gas_futures)}
Answer 5: {..., skip(fx_swap), skip(gas_futures), take(carbon_credits)}
Answer 6: {..., skip(gas_futures), take(carbon_credits), take(fx_swap)}

(Each answer also lists the candidate and conflict facts — elided here as ... for the page; run it to see them.) Six worlds, not eight: the two containing both gas futures and carbon credits are gone, and every mandate-respecting portfolio — including the empty one, a legitimate if unambitious choice — is present exactly once. The deliverable is the enumeration: hand the six to the desk, or pipe them into downstream rules that score them.

What the fence buys, in both directions

Notice what stayed and what changed at the @asp boundary — the trade is precise, not rhetorical.

Stayed: the entire linguistic frame. Same syntax, same signatures with the same compile-time protection, same reading-aloud discipline (take P if P is a candidate and you don't skip it — the rules remain sentences). Same order-independence: shuffle the file, same six answers. Termination, too, survives — the fence encloses finite worlds over declared domains, not unbounded search.

Changed: the meaning of a run. Outside the fence, a program denotes one world and every fact in it is a theorem; inside, it denotes a set of worlds, and the honest questions become “in some acceptable world?” / “in every acceptable world?” — which is exactly the vocabulary a compliance officer already uses (“is there any compliant allocation?”; “must we hold this in all of them?”). And the cost model changed teeth: finding stable models is genuinely combinatorial — this is the ground where chapter 4 measured the grounding cliff, and the fence does not repeal it; the reference solver behind today’s listing is built for correctness, not scale (chapter 10 says what division of labor the scaled architecture assigns, and to which processor). The pragma at the top of the file is thus a price sticker in exactly the ?prob tradition: you can see at the first line that this module buys expressive power with search.

Refused: the mixture. Probabilistic facts do not enter @asp modules — not because the combination isn’t tantalizing (it is, and chapter 11 touches the research frontier growing toward it) but because the mathematics of “probability over self-consistent worlds with cyclic negation” is not settled ground the way everything else in this book is, and the constitution forbids shipping an arithmetic without a semantics. Where chapter 7’s line was “no silent conversion,” this chapter’s is starker: no bridge at all, yet, and the type checker says so out loud.

The shape so far

Take stock of the language you now hold, because with this chapter its expressive frame is complete. A deductive core where everything is a theorem (chapter 6). Pluggable arithmetic over that core, with the double-counting line enforced between the arithmetics that ride the fixpoint and the ones that need the pedigree (chapter 7). And a fenced yard for genuine choice, where the semantics switches from the world to the acceptable worlds (this chapter). Three regimes, three visibly different price stickers, one syntax — and each regime’s guarantee stated on its own terms rather than averaged into mush.

What the language has not yet had to face is its intended author. Every program so far was written by me, slowly, for you. The next chapter hands the keyboard to the machine the whole design has been bracing for — and shows what the bracing was worth.

Try it.

cargo run -p strata-cli -- run examples/book/ch08-portfolio.strata

Then: (1) add a third mandate — conflict(fx_swap, gas_futures). and its mirror — and predict the answer count before running (you should get five); (2) delete the viol rule and confirm all eight worlds return; (3) add candidate(rates_basis). and watch the enumeration double.

Chapter 9 — The Language That Checks Itself

Phase-0 status: every tool invocation in this chapter — check, run, fmt, ir — is real and reproducible from the repository. The LLM transcript is illustrative: it was produced by a current model (July 2026) from the prompt shown, but models are not deterministic and yours may err differently. That variability is not a caveat undermining the chapter — it is the chapter’s entire point. Nothing below depends on the model being right.

Part I ended on an inversion: for fifty years languages were optimized for the writer, and the LLM era flips the scarce resource from writing code to trusting code someone — something — else wrote. Every design decision in the last three chapters was made with that inversion in view. This chapter finally runs the experiment: hand the keyboard to the machine, and watch which properties of the language carry the weight.

The vignette

The compliance desk receives a new mandate, in English, the way mandates actually arrive:

“Do not clear a trade if any beneficial owner of the counterparty, within two levels of ownership, is on the sanctions list.”

An engineer pastes the sentence into a model, along with the trading house’s predicate declarations, and asks for Strata-K. Back comes a draft — examples/book/ch09-vignette-draft.strata:

domain firm.

pred owns(firm, firm): Bool.
pred listed(firm): Bool.
pred counterparty(firm): Bool.
pred owner_within2(firm, firm): Bool.
pred blocked(firm): Bool.
pred cleared(firm): Bool.

owner_within2(P, C) :- owns(P, C).
owner_within2(P, C) :- owns(P, M), owns(M, C).

blocked(C) :- counterparty(C), owner_within2(P, C), listd(P).

cleared(C) :- counterparty(C), not blocked(C).

owns(apex, brightwater).
owns(brightwater, dunlin).
listed(apex).
counterparty(dunlin).

Read it before the tools do — the model has done real work here. It noticed “within two levels” means bounded recursion and correctly wrote owner_within2 as two non-recursive rules rather than copying chapter 6’s unbounded controls; it kept the stratified shape; the test facts even exercise the two-level case. It also, in the blocked rule, spelled listed as listd.

Now run the moment this book has been building toward since the design note in chapter 6. In Prolog, in an expert shell, in classical Datalog, listd is a legal predicate that happens to have no facts: blocked silently never fires, and the program clears every counterparty on the sanctions list — the worst possible failure, deployed with green tests unless a test happens to cover the typo. In Strata-K:

$ strata check examples/book/ch09-vignette-draft.strata
error[E1001]: predicate `listd` is used but never declared
  --> 16:1
   | blocked(C) :- counterparty(C), owner_within2(P, C), listd(P).
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

A stable error code, the offending line, the span. Feed exactly that text back to the model — this is the repair loop from chapter 5’s line five, and the error message is its fuel — and the fix comes back one token wide. strata check now reports ok; then:

$ strata run examples/book/ch09-vignette.strata
blocked(dunlin)
counterparty(dunlin)
listed(apex)
owner_within2(apex, brightwater)
owner_within2(apex, dunlin)
owner_within2(brightwater, dunlin)
owns(apex, brightwater)
owns(brightwater, dunlin)

The engineer’s last step is the English gloss, and it writes itself off that fact list, because the derivation behind the verdict is three facts long: dunlin is blocked because apex owns brightwater and brightwater owns dunlin — so apex is an owner within two levels — and apex is listed. Hold that against the original mandate sentence. An auditor can check the one against the other clause by clause, which is the property the prologue said a regulated industry is entitled to and imperative code cannot give: not a diff of implementations, but a correspondence between a rule as stated and a conclusion as derived.

That is the whole loop: requirement in, rules out, defect caught by the checker rather than the production incident, repair driven by a named error, result explained in the vocabulary of the requirement. One pass through it is anecdote; what makes it an argument is why each step held. So — the property walk.

Why the typo could not survive

Mandatory signatures, chapter 6’s design note, now with the payoff banked. Note precisely what saved the run: not model intelligence, and not test coverage — the grammar of the language made “predicate that exists nowhere” unsayable. LLMs are pattern engines; their characteristic failure is the plausible near-miss — listd, a swapped argument pair, an arity off by one — and this language was shaped so that the plausible near-miss class lands, structurally, in compile errors instead of silent semantics. You cannot make a model stop typo-ing. You can make a language in which typos have nowhere to hide.

The error the checker cannot see

Honesty demands the second act, because the first one can leave a false impression: that strata check is the safety net. It is the first net. Here is a draft the model could just as plausibly have produced — identical to the repaired program except for one rule, where the arguments of owner_within2 arrive swapped:

blocked(C) :- counterparty(C), owner_within2(C, P), listed(P).

Both arguments are firms; the types match; the arity matches; nothing is undeclared. strata check reports ok — as it must, because this program is perfectly well-formed. It just answers a different question: “is C blocked when C owns someone who is listed” instead of “when someone who owns C is listed.” Ownership, upside down. Run it:

$ strata run examples/book/ch09-vignette-draft2.strata
cleared(dunlin)
...

Dunlin — owned, two levels up, by a sanctioned firm — walks free. This is the plausible near-miss in its most dangerous form: past the type checker, wearing green.

What catches it is the next layer down, and the mandate itself supplied the net: every compliance requirement arrives with worked examples, or can be made to — “Apex is listed, Apex owns Brightwater owns Dunlin, therefore Dunlin must be blocked” is precisely such an example, and it was sitting in the draft’s own test facts. Assert it — expect blocked(dunlin) — and the swapped version fails loudly. The crucial point is why this test is trustworthy here in a way integration tests never quite are in imperative code: the language is deterministic and order-free, so when the expectation fails there is exactly one suspect — the rules. Not flaky scheduling, not test-ordering, not a stale cache: the rules. A disagreement between a worked example and a fixpoint is a fact about the program, and the repair loop can consume it just as it consumed E1001.

So the verification stack is layered, and each layer catches what the one above cannot: the schema catches malformed structure, the signatures catch the unsayable, stratification catches the paradoxical, and worked examples catch the well-formed lie. Layer four exists in every language, of course — it’s called testing. What the language contributes is that layer four here is cheap and conclusive: milliseconds to run, deterministic to interpret, with the pedigree (chapter 7) available to show exactly which rule chain produced the wrong verdict. The draft’s swap, unfolded, reads “dunlin is cleared because no owner of dunlin is listed — wait, the rule asked whom dunlin owns” — and the bug explains itself in the mandate’s own vocabulary.

Why order never entered the conversation

The model emitted declarations, rules, and facts in whatever order its sampling produced. Nobody checked; nobody needed to. In the language of chapter 4’s autopsies: Prolog’s meaning-depends-on-order would have made that same generation a lottery ticket — recall that reordering two logically identical clauses produced the silent forever-hang, the one failure mode a repair loop cannot even see, because there is no error text to feed back. Order-independence converts a whole class of generation accidents into non-events. It also makes program assembly safe: rules generated today concatenate with rules generated last sprint, in any order, and the fixpoint is the fixpoint.

Why the review was readable

The unit the human reviewed was a rule — one sentence, readable aloud, checkable against one clause of the mandate. That granularity is a language property, not a model property: the grammar has no long-range state, no rule can reach into another, and each rule’s meaning is complete on its face given the signatures. Compare the review unit you’re used to: a 40-line method where the mandate’s clause 2 is smeared across a guard, a cache invalidation, and an early return. The language’s smallness — a couple dozen productions, no methods, no inheritance, no lifecycle — is not primitivism; it is the same design pressure that made the checkable unit and the stated unit coincide.

There is a second face to this smallness, machine-facing rather than human-facing. Every Strata-K program has one canonical spelling — strata fmt is not a style vote, it is the projection — so diffs are semantic, never cosmetic, and a model regenerating a file cannot flood review with whitespace noise. And underneath the surface syntax sits the actual source of truth: a JSON document (the “High-IR”), schema-published, that the surface merely renders. strata ir converts both ways:

$ strata ir examples/book/ch09-vignette.strata --to json
{
  "ir_version": "0.1.0",
  "items": [
    { "kind": "domain",    "data": { "name": "firm" }, ... },
    { "kind": "predicate", ... },
    ...

A model — or a pipeline — can skip surface syntax entirely and emit schema-validated IR, with structural validity guaranteed by the schema check before the type checker even wakes. Two authoring formats, one meaning, mechanical round-trip: the language meets its machine authors on their terms, and its human reviewers on theirs.

Why the loop converges

Every diagnostic carries a stable code (E1001 is E1001 forever — prompts, docs, and tooling can rely on it), a span, and, where the fix is mechanical, a machine-applicable suggestion. The check itself is total and deterministic: same file, same verdict, every time, in milliseconds — which means the repair loop’s feedback signal is clean. Contrast the feedback signals chapter 4 catalogued: a hang (no signal), a bare UNSATISFIABLE (a signal with no gradient), a wrong-but-plausible answer (a signal you discover in production). A generation loop is a control system; it converges when errors are prompt, local, and named, and diverges when they are late, global, and mute. That single sentence is most of Strata-K’s LLM story, and not one word of it required the model to be good.

And the loop has a floor the model cannot fall through — you watched it hold, two sections ago, when the swapped-argument draft sailed past check and was stopped by a three-fact worked example. The stack — schema, types, stratification, examples, then the human reading the rules that survived — is cheap at every layer because the language was shaped to keep it cheap, and each layer’s verdict feeds the same repair loop.

The division of labor, stated plainly

Notice what was never claimed in this chapter. Not once did the language make the model smarter, and not once did the argument depend on trusting the model. The claim is the constitution’s third invariant, wearing its LLM clothes: nothing soft decides; soft things propose, and the symbolic core disposes. The model proposes rules; the checker and the fixpoint dispose. In chapter 11 the same sentence reappears with “neural network” in place of “LLM” and the trading house’s data flowing through it — it is one principle, and this chapter was its cheapest, most reproducible demonstration.

The demonstration also quietly used up the last of the language’s introduced-but-unproven claims. Chapters 6 through 8 showed the three regimes; this chapter showed the authorship story they were shaped for. What remains is the part of the design you cannot run today — the engine the core was shaped for, and the road that gets there. Two chapters: the iron, and the road.

Try it. Reproduce the whole vignette:

cargo run -p strata-cli -- check examples/book/ch09-vignette-draft.strata   # the catch
cargo run -p strata-cli -- run  examples/book/ch09-vignette.strata         # the repaired run
cargo run -p strata-cli -- ir   examples/book/ch09-vignette.strata --to json | head -20

Then go one better than the transcript: paste the mandate sentence and the pred declarations into the model of your choice, and run its draft through strata check. Your error will differ from mine. The loop won’t care — that’s the point.

Chapter 10 — Iron

Status, stated at maximum bluntness. The engine this chapter describes is designed and not built. What exists today is the CPU reference implementation you have been running since chapter 6 — deliberately slow, deliberately obvious, exhaustively cross-checked. This chapter therefore contains not a single benchmark number, and any figure you meet is an asymptotic or architectural claim, not a measurement. What it offers instead is the design rationale: why the language of chapters 6–9 is shaped so that this engine can exist, and why the shape of modern hardware makes the bet reasonable. When the engine ships, its numbers will be published against the reference oracle described at the end — that commitment is part of the design.

FGCS spent a decade and a national budget learning that you cannot build hardware for a logic language whose execution model is a sequential walk. Chapter 2 promised the inverse was now possible — a logic language built for hardware that already exists. This chapter pays that promise out, in four decisions.

Decision one: the unit of work is a pass, not a step

Recall what running a Strata-K program is: apply every rule to everything known, collect the new facts, repeat until nothing new appears. The imperative mind pictures that as a loop over facts — pop one, extend it, push the results; that was the worklist of chapter 1, and one-at-a-time is precisely the shape a GPU cannot use.

But nothing in the fixpoint’s definition says one at a time. A pass can take the entire set of known facts and apply a rule to all of it simultaneously: a rule body like owns(X, Y), controls(Y, Z) applied in bulk is a join of two tables — the same operation your database’s planner executes — followed by projection and deduplication. Set in, set out, no fact’s processing depending on any other’s within the pass. That is what “embarrassingly parallel” meant every time Part I used the phrase, and it is a property of the branch: the fixpoint family computes over sets, where the search family (Prolog’s SLD, ASP’s solver core) walks one path of a tree, backtracks, and walks another — inherently one-after-another, meaning attached to the walk’s order. The parallelism was never something to add to Datalog. It was in the definition, waiting thirty years for hardware with enough lanes — and the delta trick from chapter 1 survives intact: each pass joins only against facts new since the last pass, so the engine does bulk work without redundant work.

Decision two: facts live in columns, sorted

How the facts sit in memory decides whether the lanes starve. A GPU is a memory-bandwidth machine: thousands of lanes reading adjacent addresses fly; the same lanes chasing pointers crawl. So the design stores each relation as sorted, compressed columns — all the first arguments contiguous, then all the second arguments — with every constant dictionary-encoded to a fixed-width integer. owns(apex, brightwater) occupies a few bytes across two integer columns, join keys compare as integers, and a bulk join streams through memory in the access pattern the hardware was priced for. If this sounds like what your analytics warehouse did to your row-store — same move, same reason. The full relation and the current pass’s delta are kept separately (sorted runs, merged after each pass), which is the storage-level shadow of the delta trick; and one consequence of chapter 6’s design quietly pays off here: facts are never updated in place — the model only ever adds — so the storage never faces the concurrent-mutation problem that makes parallel imperative code miserable.

Two further consequences of the language design land in this section. Mandatory domain declarations mean every column’s value universe is known and dense — dictionary encoding is not an optimization pass, it falls out of the type system. And the absence of term construction (chapter 1’s “no new”) means a fact is always a fixed-width tuple of scalars: nothing variable-length, nothing heap-shaped, nothing to chase. The language was kept small in exactly the places that would have broken columnar storage.

Decision three: plans are chosen, not worshiped

A rule body is a small query, and queries have plans. For most bodies the classic strategy — a pipeline of pairwise joins, cheapest first — is right. But some shapes defeat it: a body asking for triangles (r(X,Y), s(Y,Z), t(Z,X)) can produce enormous pairwise intermediates that the third condition then throws away, and for such cyclic cores the design uses the newer strategy chapter 5’s frontier proved out — walking three sorted relations simultaneously, intersecting as it goes, never materializing the doomed intermediate. The planner’s rule is unglamorous: decompose each rule body, give the cyclic core the simultaneous walk, give the acyclic remainder the pairwise pipeline, decide by estimated cost. No single-algorithm dogma — the autopsies of chapter 4 were one long lesson in what dogma costs. (The same pragmatism, incidentally, is why the design’s most speculative idea — executing small dense sub-joins as tensor operations on the GPU’s matrix units — is explicitly fenced as a last-phase optimization, legal only where measured density justifies it. Early drafts of this project made tensor contraction the foundation; the critical review that produced the current design demoted it to a footnote. Constitutions exist because first drafts don’t survive contact.)

One engineering constraint shapes every kernel in the design: GPU code cannot allocate memory mid-flight the way host code does. So every materialization is two-phase — a light pass counts exact result sizes, a prefix sum turns counts into offsets, a heavy pass writes into pre-sized buffers. Deterministic, allocation-free, and — a property this book cares about more than most engine papers do — bit-reproducible: the same program on the same facts produces the same relations, to the byte, run after run. Determinism is not a debugging luxury here; it is what makes the correctness story below possible at all.

Decision four: three processors, three jobs

The full system, GPU alone can’t be. Chapter 8’s stable-model search is combinatorial choice — propagate, guess, learn from conflict, backtrack — and its core is exactly the sequential, branchy, latency-bound computation CPUs are built for and GPUs are worst at. Pretending otherwise would repeat FGCS’s category error in mirror image. So the division of labor is explicit, and it is the architecture the whole book has been drawing one panel at a time:

• GPU: everything set-shaped — the deductive fixpoint (chapters 6–7), the massive grounding step that chapter 4 measured as ASP’s entry wall, pedigree capture, and the bulk simplification that shrinks a combinatorial problem before search ever sees it.
• CPU: everything path-shaped — the stable-model search itself (chapter 8), circuit compilation’s hard steps (chapter 7’s mode B), orchestration.
• Neural hardware, eventually: everything heuristic — proposals for which branch to try first, candidate answers to verify. Under the constitution’s third invariant, never deciding — a neural hint may reorder the search, and may not change what the search accepts. Chapter 9 showed that principle with an LLM; here it is again with a GNN, unchanged.

Notice the shape: it is chapter 4’s autopsy table, inverted into a deployment diagram. Each paradigm’s “fundamentally sequential part” — the thing that killed its parallel ambitions — is assigned to the processor that likes it, instead of being asked to vanish.

The part that keeps it honest

Now the question this chapter must not dodge: when the fast engine exists, why should anyone believe its answers?

Because the slow engine exists first, and that ordering is the point. The reference implementation you have been running — naive fixpoint, then an independent semi-naive engine, cross-checked against each other, against an external engine on the shared fragment, and against exhaustive-by-construction oracles for probability and stable models, over tens of thousands of fuzzed programs — is not a placeholder awaiting deletion. It is the specification, executable. The constitution’s fifth invariant binds the GPU engine to match it: bit-for-bit on Bool, within declared tolerance on numeric semirings, on the same corpus plus differential fuzzing, forever. A performance claim without an oracle is marketing; Phase 0 was built slow-and-obvious first precisely so that every fast thing after it has something unforgiving to answer to.

And because others are already proving the direction, the claim “Datalog rides GPUs” no longer rests on this project’s word alone: the research engines chapter 5 cited have published order-of-magnitude results for exactly the bulk-join fixpoint architecture described here. What no one has yet shipped is that architecture carrying this language — semirings, pedigrees, the mode split, the fenced choice layer — which is Strata-K’s actual wager, and it remains a wager until the code exists. You have my status box; hold me to it.

The design is now fully on the table — language, semantics, authorship story, iron. One chapter remains: the road from the repository you can clone today to the system this chapter described, and the honest map of what’s known, what’s designed, and what’s still research.

Chapter 11 — The Road

Status: this chapter is the one the status boxes have been deferring to. Everything in it is design or vision, explicitly staged; the only executable things here are the ways today’s tools already acknowledge tomorrow’s syntax.

Every claim in chapters 6 through 9 you could run. Chapter 10 was design with an oracle waiting for it. What remains is the part of the project that is honestly a bet — and the prologue promised that when this book speculates, it says so. This chapter says so. It also says something rarer: exactly which pieces are settled engineering, which are designed-but-unbuilt, and which are open research, because those are three different kinds of promise and mixing them is how fields earn winters.

The boundary where the network lives

Start with the piece the whole design has been shaped around and has never yet shown: the neural predicate. Try it today:

$ strata check examples/book/ch11-neural.strata
error[E0100]: neural predicates is not implemented in Phase 0
  --> 3:1
   | neural flag(firm, label) from model "aml_gnn".
   | ^^^^^^

Read that diagnostic carefully, because it is doing something unusual. The declaration parsed — the grammar of the full language, neural predicates included, is already the shipped grammar, and unbuilt features are refused by name with a stable code, not rejected as gibberish. The surface is complete; the execution is staged. That is what a future-syntax frame means mechanically, and it is a small design decision with a purpose: programs written against the full language today fail loudly and specifically, never silently and confusingly — the same courtesy the language extends to typos, extended to its own roadmap.

Here is what the declaration will mean, and it costs one sentence because every concept in it is already yours: flag is a predicate whose facts arrive not from the file but from a model’s inference — each fact annotated with the model’s confidence, exactly as chapter 7’s probabilistic facts were annotated — flowing into rules that treat it like any other soft evidence, behind the same mode-B line, with the same taint discipline: anything derived from it is marked soft in its signature, forever, by the type system. The network proposes; the rules dispose. An anti-money-laundering screen in this style is: a graph model flags suspicious structures with confidences; hard rules — the kind chapters 6 and 8 taught — take the flags as probabilistic input and derive investigate(X) with a pedigree; the pedigree distinguishes “flagged by the model” from “derived from ownership facts” in the type of the conclusion. The auditor sees which part of the answer is theorem and which part is opinion. No fragment in chapter 3, and no system in chapter 5 short of the research frontier itself, offers that sentence.

And the gradient flows back. The pedigree circuit of chapter 7 is differentiable — run backward, it tells the model how much each of its confidences mattered to the conclusion — so the training loop of the host framework can teach the network through the logic. That is the design’s participation in the neuro-symbolic convergence of chapter 5, borrowed pieces credited there; ?grad, parsed and staged like everything else, is its query form.

The phases, and the kind of promise each one is

The road from the repository you can clone to the system of chapters 10–11, in the order the engineering dependencies dictate — with each phase labeled by promise-kind: [E] settled engineering (the field knows how; it’s work), [D] designed here, unbuilt (chapter 10’s kind — an oracle exists to hold it honest), [R] open research (no one knows; declared as such).

1. Scale the pedigree machinery. Circuit compilation for exact probabilistic queries beyond toy size [E — the knowledge-compilation field’s standard toolbox], and top-k pedigrees for recursive programs, the declared lower-bound approximation credited in chapter 5 [E, borrowed with attribution].
2. Incrementality. New facts arrive, conclusions update without recomputation — the differential machinery chapter 5’s line three proved out, applied to this language [E in the literature, D in this design]. For the trading house this is the difference between a nightly batch and a compliance engine that answers during the trade.
3. The GPU engine. Chapter 10, executed: columnar fixpoint, hybrid planner, the three-processor split [D, oracle in hand, related work already demonstrating the direction].
4. The neural boundary. Predicates from models, gradients back through pedigrees [D at the interface; E for the pieces it borrows; the integration at production scale honestly sits between D and R].
5. Structured values — @terms, the fenced extension that trades away guaranteed termination for constructor terms (lists, trees) with declared-incompleteness controls [D, and the fence is the design].
6. The bridges that don’t exist yet [R, plainly]: probability across the @asp fence — the semantics of “likelihood over self-consistent worlds” — is an open research area, and this book has already told you (chapter 8) that the type checker refuses the combination rather than improvise it. If the field settles it, the fence gets a gate. Until then, the constitution holds: no arithmetic without a semantics.

What is deliberately not on the road: nothing from chapter 5’s refusals has crept back. No theorem proving, no continuous-domain constraint solving, no training framework, no general-purpose ambitions. The road makes the language more of what it is, not more things.

Where this leaves you

The prologue asked you to carry one thing through eleven chapters: your own version of the sanctions smear — the rule in your codebase that is everywhere and nowhere. Here is the whole journey, measured against it.

The rule can be written as what it is — chapter 1’s bargain, chapter 6’s thirty lines, readable by the officer who owns it. It can carry cost and likelihood without lying about either — chapter 7’s one word, and the line it refused to cross. It can face genuine choice — chapter 8’s fenced worlds. It can be drafted by a machine and caught when the draft is wrong — chapter 9’s one-token repair, the loop that never asked the model to be trustworthy. It can, when the road is walked, run at the speed of the hardware your industry already owns — chapter 10’s bet, honestly boxed. And at every step, the answer can show its work: the pedigree, the derivation an auditor can hold against the regulation, clause by clause. Programs that know why.

The third bet is placed in the open — the spec, the reference implementation, every listing in this book, and the differential harness that keeps the fast future honest all live in one repository, and the phases above are its issue tracker, not a prophecy. Clone it. Run the trading house. Break the checker; read its errors; feed a mandate of your own to a model and see what survives strata check. FGCS teaches that this paradigm’s bets die of arriving before their hardware; chapter 2 argued the hardware has finally arrived, chapters 6 through 9 put the language in your hands, and the only piece of the argument no book can supply is the working engineer who tries the fifty-year-old idea on this decade’s problem and decides, on the evidence, whether it holds.

That’s you, and the repository is open. The rules, at last, can be the program.