Why DKE is built this way
An answer you can't check is a rumour with better grammar. Most systems resolve contradictions before you see them, discard the question of who said what, and can't tell you what a record said last March. DKE refuses all three — structurally, not as policy.
Provenance has to be structural, not optional.
A system that can record an unattributed fact eventually will. DKE has no verb that writes a value without naming its source — not as policy, as grammar. An unattributed fact isn't disallowed; it's unsayable.
The cost of the alternative is already on the record. In June 2023 a federal judge in New York sanctioned the lawyers in Mata v. Avianca for a brief citing court decisions that ChatGPT had invented. Scholarship answered the same problem long ago with the footnote, whose history Anthony Grafton wrote in The Footnote: A Curious History.
Disagreement is information.
When two sources contradict each other, most systems resolve it before you ever see it — usually by whichever ranked higher. That is the most valuable thing the store was holding, discarded silently. DKE keeps both claims live, counts the sources behind each, and makes you decide.
Law has known this for a long time. The Mishnah asks why it records the opinion of a single sage beside the majority's, when the law follows the majority, and answers: so that a later court may rely on it. The common law keeps its dissents for the same reason. Justice Harlan wrote alone in Plessy v. Ferguson in 1896 that “our constitution is color-blind,” and Brown v. Board of Education was widely seen in 1954 as his vindication.
Time is not metadata.
“What did this record say last March” is the question audits are made of. Its most famous form was Senator Howard Baker's at the Watergate hearings in 1973: “What did the President know, and when did he know it?” It shouldn't require a separate warehouse to answer. In DKE, writes carry a validity window and reads carry an as-of instant — the history is the store, not a copy of it.
A system that can't be made to halt can't be relied on.
DKE's language has no while, no recursion, no unbounded loop. Every program terminates, and the same program over the same store gives the same answer. Not a feature — a property you can't switch off. Nothing an agent emits can hang the engine, because there is no unbounded loop to emit.
It has followed since Alan Turing's 1936 paper on computable numbers that no general method can tell, for every program, whether it will ever stop. So the guarantee can't be checked afterwards. It has to be built into what the language can say.
We publish the contract and keep the engine.
The language specification is MIT and versioned. Write a linter, a formatter, a language server, a competing compiler — the published document is the whole surface, and we're held to it. Your programs, and everything you build around them, outlive any decision we make.
The internet's protocols have been written this way since Steve Crocker's RFC 1 in 1969: the document is public, and anyone may build to it. Hyrum's Law says why the contract has to be written down. With enough users, “all observable behaviors of your system will be depended on by somebody,” so the contract is what tells them which ones are promised.