The destination format
If the model is a compiler, something has to be the target language. The criteria are not the obvious ones.
What makes a target language good here: decidable and terminating, so you can state a worst-case cost and mean it. Analysable, so a solver can answer questions about the policy rather than about one execution. Attributable, so the engine can say which rule fired on which facts. Readable by the person who owns the intent. And small enough that a model reliably generates valid programs.
Analysability and readability pull against expressiveness and against each other. That tension is the design space.
The most interesting artifact in this space is an authorisation language whose design brief made analysability an input rather than a retrofit: "finely balanced to allow for a sound and complete logical encoding, which enables precise policy analysis, e.g., to ensure that when refactoring a set of policies, the authorized permissions do not change." It is modelled in a proof assistant and important properties are proved.
- Termination by exclusion. No loops. Worst case quadratic, common case linear.
- Proved order independence — the order you write policies in cannot change the answer. That single property eliminates a whole class of rules-engine bug and makes policy sets composable and diffable.
- A validator that warns on conditions that can never be true, which is a coverage check falling out of the type system.
- A symbolic compiler producing concrete counterexamples, with the hard part solved: converting infinite solver models into finite, hierarchy-valid inputs a human can read.
- Differential random testing of the production implementation against the definitional model, continuously.
A decision table declares hit policy Unique. Two rules match one input. What happens, and why is it good?
The rest of this lesson unlocks when you commit above.