What the formalizer’s work leaves you with

You have the text of an act and a question that people ask of it again and again. Today there are four ways to answer it. Ask a lawyer. Write a program in which the act’s conditions became if branches. Build an expert system. Ask a language model. Each way yields an answer. None of them leaves an object you can put on the table, check, change in one place, and ask again a year later under the same law.

Formalization leaves that object. That is the return, not that a machine “understands the law”: it does not. What follows shows, on one small case, what remains after the work and why the effort is worth it when it is.

Arxo executes the canon. Models formalize; two engines execute and prove.

One question, asked three times

Archive rules, item 4: “A reader is admitted to the rare-holdings room if they are on the researchers’ register and hold a valid accreditation.” Researcher Ivanova is on the register. She is accredited at another state archive.

A lawyer will answer: it depends how one reads “valid accreditation.” Literally — only this archive’s accreditation, and there is no admission. Extensively — accreditation at any state archive is recognised, and there is admission. Practice diverges; the text is silent. That is an honest answer, and it is one-shot: next time the lawyer will reason again, another lawyer differently, and the dispute over how to read remains a dispute in the air.

The formalizer records the same thing, but so that it stops being air. The undisputed part — that this archive’s own accreditation counts, and that admission requires the register and an accreditation — becomes ordinary norms. The disputed part is recorded twice: as a rule “out-of-town accreditation is recognised” and as a rule “out-of-town accreditation is not recognised.” Both rules exist in the package, but each is attributed to its own reading of item 4, and the item is marked as disputed. The author takes no decision about who is right.

Now Ivanova’s case can be asked three times.

What the case selects	Answer to “is Ivanova admitted”	Why
no reading selected	the law is silent	disputed rules are inactive; the undisputed ones do not suffice for admission
reading A, literal	refusal	accreditation at another archive is refuted by this reading
reading B, recognition	admission	accreditation is recognised, the register is there

Three answers on the same facts, and each names a reason. The first of them is the most important, and it is not “no.” It says: the package did not resolve the dispute, and the one entitled to resolve it must do so — a court, an agency, a contract. Select a reading, and the answer changes to “yes” or “no” without a single edit to the rules.

All three rows are not an illustration but scenes the engine executes on every repository check: they are recorded in the tutorial on readings and fail if the language or the package changes. There is a fourth scene there as well: Ivanova with this archive’s accreditation is admitted under any selection and without one. The undisputed part was not damaged by honestly calling the disputed part disputed.

What remains on the table

After the formalizer’s work three things remain, and neither a consultation nor a program with if branches leaves any of them.

A model of a reading. Not “law in code,” but a recorded reading of a particular text in which every norm carries the address of an article in a document pinned as bytes. A dispute about the model is a dispute about a text you can produce, not about a page that is already different at the former link.

Scenes. The facts of the case and the expected answer, recorded together: “the register is there, accreditation is out-of-town, no reading selected — the law is silent.” A scene is at once a check of the model and its documentation: it says what the author meant, in a language the machine executes and a lawyer reads.

An answer with grounds. To each question the engine returns not “yes” but a document: a status, the rules that applied, the address of each norm in the source, which premise is not established if there is no answer, and hashes by which the same answer is reproduced later under the same law. The answer becomes an object that can be contested part by part.

What remains with the human: the choice of reading, the facts of the case, and every judgment the act left to an organ — “reasonable time,” “good cause,” “material breach.” The machine does not compute those; it answers that without them there is no answer, and names whose decision that is.

How this differs from what you already have

The comparison is honest: each of the four tools can do much of what is listed, and to claim otherwise would be untrue. The difference is that here all of it is one shared contract, checked by gates, not an agreement inside a single project.

Tool	What it gives	What it does not leave	How it is otherwise here
Lawyer and text	a reading that takes account of everything a machine cannot reach	a reproducible answer; the dispute about the reading stays oral	the reading is recorded and producible; the lawyer selects it rather than retelling it every time
Program with if branches	speed, integration, any semantics you write	the distinction among “no,” “unknown,” and “disputed”: a branch has two outcomes; branch order silently becomes priority	four support statuses, exceptions without else, seniority of norms only with a named ground, edition and legal date as input
Expert system	rules, explanations, non-monotonic inference	pinning of the source, positions with a life cycle, several readings of one text, an independent second implementation	the same class of machine, but with a legal contract: source, time, duty, reading, proof, two implementations on one document
Language model	a fast draft, similar-text search, an explanation in its own words	determinism, addresses of norms, reproducibility; the answer cannot be taken apart by premises	the model helps propose a formalization; a human selects the reading; the engine computes the consequences of what was selected — three jobs, not one

The first row matters more than the rest. Formalization does not replace the lawyer: it gives the lawyer an object on which their choice is visible, checkable, and outlives the consultation.

When this is not needed

The formalizer’s work is not always justified, and an introduction is obliged to say when it is not.

• The question is asked once. Taking the text apart for a single answer costs more than asking a lawyer.
• The norm is simple, undisputed, and does not change. A calculation by one formula with known inputs lives perfectly well in ordinary code; four statuses and readings do nothing for it.
• The source cannot be pinned: there is no official text that can be produced as bytes. A model without a producible source is an opinion.
• The decision is almost entirely evaluative. If every premise requires an organ’s judgment, the machine will honestly answer “a decision is needed” to every question, and that will be true, but not help.

The return appears where the question repeats, rules change by edition, readings dispute, and the cost of error is such that the answer must be take-apartable by grounds. Registers, permits, deadlines, contributions, admissions — that is it.

Next

The four articles that follow explain why the language is built this way, before any syntax: why there are four answers, not two; why an exception does not reduce to else; why “must return” does not mean “returned”; what must be kept so that an answer can be repeated. After them — the first tutorial, where the archive package is assembled from scratch. For someone who only wants to ask questions of already formalized law, the introduction is not needed: their path is the guide.