Policy as Code, Policy as Type

Matthew D. Fuchs

REVIEW 3 major objections 7 minor 19 references

Policy as Code, Policy as Type

T0 review · 3 major / 7 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A policy is a dependent type: code that cannot construct a proof of compliance will not type-check, moving access-control enforcement from runtime checks to compile-time proofs.

desk verdict A useful worked illustration of policies-as-dependent-types, but the paper overclaims generality, misses prior art on proof-carrying authorization, and leaves a real determinism gap unaddressed. read the letter →

arxiv 2506.01446 v1 pith:RS6EICRL submitted 2025-06-02 cs.CR cs.PL

Matthew D. Fuchs This is my paper

classification cs.CRcs.PL

keywords policyastypedependenttypesattribute-basedaccesscontrolAgdaLeanRegocompile-timeverificationverifiablecredentials

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that an access-control policy can be encoded as a dependent type in a language like Agda or Lean, so only code that carries a proof of compliance will type-check. This turns policy enforcement from a runtime check into a compile-time guarantee, and it lets the language's proof assistant verify not just individual decisions but properties of entire policy sets. The paper demonstrates the idea by re-encoding the introductory examples of Rego, an open-source attribute-based access control (ABAC) language, and by modeling a video-service policy involving age limits, parental permission, channel safety, and service approval. If the approach works in practice, ABAC systems gain the strongest available correctness guarantee, and the same types can carry signed claims in a distributed setting.

What carries the argument

The central machinery is the propositional dependent type, a type whose inhabitants are proofs and whose form can depend on the values it talks about—for example, the claim that one number is at most another is a type, and constructing an inhabitant is constructing a proof. In the paper, each policy is such a type (SafeSender, SafeChannel, SafeService, and so on); its constructors are the policy rules, dependent pairs bind an entity together with a proof of its policy, and a decidable oracle lets code test whether a proof exists. This puts the type checker in the role of the enforcement point and lets the proof assistant verify meta-properties such as protocol categories being exhaustive and exclusive.

What would settle it

Take a realistic ABAC policy that includes an external lookup or a sliding-window transaction limit, encode it in Agda following the paper's method, and check whether the encoding remains faithful and terminating; if some such policy cannot be encoded as a decidable dependent type, or if an Agda proof can be constructed for an action the original policy would deny, the central claim fails.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that a policy is a type: a policy over senders, receivers, messages, and context is a propositional dependent type, and a term of that type is a proof that a particular action satisfies the policy. In the Agda implementation, policy rules become type constructors, decisions become proof obligations, and functions such as safeCall accept only dependent pairs that bundle an action together with its compliance proofs. Because the type checker verifies these proofs statically, any code path that fails to establish the policy cannot reach the protected operation; the same mechanism also yields regression proofs, proofs of invariants, and proofs about policy definitions themselves. The paper argues this exceeds the guarantees of Rego, Cedar, XACML, and Sentinel, and sketches how the same types can transport signed claims in a verifiable-credential world.

Load-bearing premise

The load-bearing premise is that every real-world ABAC policy of interest can be faithfully expressed as a decidable dependent type in Agda or Lean; otherwise the compile-time guarantee certifies only the formal encoding, not the intended policy.

Editorial extensions

If this is right

ABAC policies written as types are enforced at compile time, so a code path that cannot construct the required proof never reaches the protected operation.
Policy properties that today are checked by regression tests—such as every protocol falling into exactly one category—can be proved once, and the build fails if policy changes break the proof.
Longer stretches of code involving several policies can be proved to maintain invariants, because the proof assistant can reason about types across calls.
In a distributed setting, the client can gather signed claims and a proof sketch, and the server needs only to validate the proof rather than assemble all attributes itself.
Because a policy exists as a logical specification separate from its implementation, the same types can be translated for analysis with SAT solvers and model checkers.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The paper leaves implicit that policy updates become proof-repair tasks: changing a policy changes its type, so existing call sites and proofs stop compiling until updated, which strengthens regression protection but creates rework the paper does not quantify.
A direct testable extension is to automate the proof-finding and proof-serialization functions from policy types—the paper mentions auto-generation only in passing—and measure whether that automation scales to industrial-size policy sets.
The same policy-as-type encoding could serve any validation problem with cross-field constraints, such as configuration schemas or contract conditions, not just access control, since the mechanism only requires a decidable propositional type.
A bridge to near-term practice would be annotation-based checkers in mainstream languages, which could give partial compile-time enforcement without requiring teams to adopt a full dependently typed language.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's my take. The paper argues that authorization policies should be written as dependent types in Agda or Lean, so that a request is a proof term and serving code only accepts proof-carrying requests. That idea is not new — proof-carrying authorization and richly typed policy frameworks have been around for a while, and the paper doesn't cite any of them — but the concrete Agda encodings are a useful worked illustration. The 'regression proof' idea, proving invariants over the policy model (e.g., every protocol is categorized exactly once) is a nice bonus. The Rego head-to-head is mostly rhetoric, but the point about Rego's oracle/sidecar gap is fair: with dependent types the policy check is woven into the call itself.

Where does it get soft? The central claim is 'even the most complex ABAC policies can be expressed as types.' What is shown is a handful of small examples: an intersection check, a movie-permission policy, a transaction policy. There is no general translation from Rego-style rules to dependent types, no discussion of which policy classes are encodable when attributes are dynamic or open-ended, and no machinery for policies that intentionally return 'undefined' when no rule applies. The paper collapses 'the query does not typecheck' with 'the policy denies the request.' In constructive type theory, absence of a proof is not proof of denial. The Maybe-returning safeCall just drops the request; it doesn't prove the request is not permitted. The determinism gap the stress-test note raises is real and not addressed.

Also, the Agda code as printed looks incomplete and inconsistent. StrongProtocols is defined as including http, contradicting the text saying strongProtocols is 'everything else' with weak protocols excluded. That is exactly the kind of error the compiler would catch, so either the code was not what was compiled or the paper was not machine-checked as printed. The paper should ship a repository and say which definitions are actually checked.

The paper also reaches for 'most complex decidable policies' and 'superior safety' without benchmarks or a formal semantics for the translation. That overclaim is manageable with revision.

Verdict: this is a decent position paper with real code sketches, but as a scientific contribution it needs a serious referee to discipline the claims and the related work. I'd send it to review; I'd expect major revision. I would not cite it yet. Bring it to the reading group if you want a discussion about dependent types in policy engineering, not if you want a rigorous result.

Referee Report

3 major / 7 minor

Summary. The paper proposes 'Policy as Type' (PAT): formalize ABAC policies as propositional dependent types in Agda, so that a term inhabiting the policy type is a proof that an action satisfies the policy, and the type checker enforces policies at compile time. The paper argues that this provides provable correctness for complex policies, compares PAT with Rego, Cedar, Sentinel, and XACML, and demonstrates the idea on a server-configuration example and a video-transaction example with SafeSender, SafeChannel, and related dependent types. It also sketches extensions to distributed verifiable claims, stateful event-loop processing, and serialization of proofs. The examples are hand-written Agda; no external artifact or machine-checked development is provided.

Significance. The core observation — that a policy can be represented as a type and its enforcement as proof construction — is sound and worth stating, and the paper correctly identifies a genuine weakness of untyped policy languages: no compile-time guarantee that the policy implementation matches the specification. The paper also avoids the usual fitting circularity: there are no free parameters, and the code snippets are concrete enough to be checked. However, the paper's contribution as submitted is a vision with small illustrative encodings rather than a demonstrated systems result. The claims of 'most complex ABAC policies' and 'provable correctness' are broader than the evidence; the code contains at least one internal inconsistency; and the treatment of decidability and Rego's undefined semantics is incomplete. If the encodings were corrected, a decidability/faithfulness theorem supplied, and the code artifact made buildable, the approach would be a useful step for policy engineering, but those steps are needed before the central claims are supported.

major comments (3)

[Sec. 3, strongProtocols definition; Sec. 3.1 separate] The definition of strongProtocols includes http ('strongProtocols = https :: ssh :: mysql :: memcache :: http :: []'), even though the text says weakProtocols 'just includes http' and strongProtocols 'contains everything else.' This makes weakProtocols ∩ strongProtocols = http :: [], so the claimed proof 'separate = refl, refl, refl' cannot type-check, and allProtosAssigned would assign http to both weak and strong. Since Section 3.1 uses this exclusivity as the central illustration of regression proofs, the demonstration as written is not valid.
[Sec. 2.2.3 and Sec. 3] The paper claims 'provable correctness for the most complex decidable policies' and superiority over Rego, but it provides no general account of what class of policies PAT can express or how a Rego rule set (with its rule ordering, default decisions, and undefined results) is mapped into dependent types. The examples are self-authored small encodings; without a translation theorem or at least a precise expressiveness comparison, the head-to-head claim is not supported. In particular, the paper does not discuss whether Rego's intentional 'undefined' answer is represented as an explicit error, a third decision value, or a proof obligation.
[Sec. 4 safeCall/preCall; Sec. 3 goodServerCheck] The enforcement mechanism returns Maybe values and uses 'nothing' when no proof is found, but the paper never establishes that the policy propositions are decidable in the relevant sense. In constructive type theory, 'no proof found' is not a refutation; to conclude denial, one needs a proof of negation. For example, goodServerCheck returns nothing in cases that should be deniable, but the paper provides no theorem that for every Server either GoodServer s or ¬ GoodServer s, and similarly for SafeSender. Without such decidability/totality results, the claim that the type checker 'ensures code actually implements the policies' is incomplete: the code could reject a request merely because a proof was not constructed, rather than because the policy was proven violated.

minor comments (7)

[Abstract] The abstract has a missing period and a broken sentence: 'harm We demonstrate' should be 'harm. We demonstrate', and 'may cause not compile errors, but financial and reputational harm' should be 'may cause not compile errors but financial and reputational harm'.
[Sec. 2.2.1] 'monastic functional programming' appears to be a typo for 'monadic functional programming'.
[Sec. 2] The sentence 'This family several languages in active use' is missing a verb; it should be 'This family has several languages in active use' or similar.
[Sec. 3] The code contains scattered spacing artifacts such as 'pr o to co ls', 'g o o d s e r v e r', and 'T ra ns po rt', which make the code harder to read; a typeset or linked source file would help.
[Sec. 4.1] The 'ClaimServer' is introduced as a hypothesized entity; the paper should clarify whether this is a standard component of the W3C Verifiable Credentials model or a new assumption, since the W3C model does not define ClaimServers as such.
[Sec. 4.1] The statement 'we hope to rely on Agda's internal reflection mechanism' is speculative; the paper should mark this as an open implementation question rather than part of the demonstrated approach.
[Sec. 4.3] The self-reference 'Techniques such as those in [my dissertation]' has no bibliography entry; provide a citation or remove the reference.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the policy-as-type claim is a formal encoding proposal, not a prediction derived from its own inputs.

full rationale

The paper contains no fitted parameters, no data-driven predictions, and no importation of a uniqueness theorem from the authors' prior work. Its central claim is that ABAC policies can be expressed as dependent types; the Agda definitions and proofs (e.g., GoodServer, safeCall, allProtosAssigned) are hand-written illustrations of that encoding, and the stated guarantees follow from the type checker's formal rules rather than from assuming the conclusion. The single self-reference, '[my dissertation]' in Section 4.3, is offered only as a source of event-loop programming techniques and is not load-bearing for the policy-as-type thesis. The paper's main open problem—whether every real-world policy of interest can be faithfully encoded as a decidable dependent type—is a validation and expressiveness concern, not a circularity. Accordingly, no circular step is identified and the score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

The paper's central claims rest on assumptions about expressiveness of dependent types for policies, trust in attribute sources, and the faithfulness of the policy-to-type encoding. No numerical parameters are fitted; the main invented construct is the ClaimServer trust infrastructure.

assumptions (4)

domain assumption Any ABAC policy of interest can be expressed as a decidable propositional type in Agda.
Stated in Section 2 ('a policy is a type') and used throughout; no general construction is given.
domain assumption Attributes needed for policy evaluation are available from trusted external systems or verifiable claims.
Assumed in Section 4 ('we assume a reference to a trusted external system to provide the appropriate attributes').
domain assumption The type signature of a function captures all safety-relevant side effects, so compile-time type checking guarantees runtime policy enforcement.
Used in Sections 3 and 4; ignores that IO and interface calls can bypass the type-level discipline unless the whole system is developed in Agda.
domain assumption Agda's termination checking and decidability of the encoded propositions match the expressibility needed for real-world policies.
Section 2.2.2 argues policies must terminate; assumes all desired policies do.

invented entities (1)

ClaimServer
purpose: A trust anchor that issues signed attribute claims for use in decentralized policy proofs.
Introduced in Section 4.1; no concrete protocol, URL format, or deployment is specified, so no external falsifiable handle is provided.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Policy as Code, Policy as Type." pith.science (2026). https://pith.science/paper/RS6EICRL

@misc{pith2026250601446,
  author       = {Pith},
  title        = {Pith review of: Policy as Code, Policy as Type},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RS6EICRL}},
  note         = {Machine review of arXiv:2506.01446}
}

read the original abstract

Policies are designed to distinguish between correct and incorrect actions; they are types. But badly typed actions may cause not compile errors, but financial and reputational harm We demonstrate how even the most complex ABAC policies can be expressed as types in dependently typed languages such as Agda and Lean, providing a single framework to express, analyze, and implement policies. We then go head-to-head with Rego, the popular and powerful open-source ABAC policy language. We show the superior safety that comes with a powerful type system and built-in proof assistant. In passing, we discuss various access control models, sketch how to integrate in a future when attributes are distributed and signed (as discussed at the W3C), and show how policies can be communicated using just the syntax of the language. Our examples are in Agda.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

19 extracted references · 18 canonical work pages

[1]

ALFA YAML Profile for XACML.https://alfa.guide

work page
[2]

The Checker Framework.https://checkerframework.org/

work page
[3]

openpolicyagent.org/docs/policy-language

Open Policy Agent — Rego Documentation.https://www. openpolicyagent.org/docs/policy-language

work page
[4]

OpenFGA — Fine-grained Authorization.https://openfga.dev/

work page
[5]

Ory – Open Source Identity Infrastructure.https://www.ory.sh/

work page
[6]

Pydantic — Data Validation and Settings Management.https:// docs.pydantic.dev/latest/

work page
[7]

HashiCorp Sentinel.https://www.hashicorp.com/sentinel

work page
[8]

Styra Inc.https://www.styra.com/

work page

Show all 19 references

[9]

W3C Verifiable Credentials Working Group.https://www.w3.org/ 2017/vc/

2017
[10]

Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells. Cedar: A new language for expressive, fast, ...
[11]

Leonardo de Moura, Sebastian Ullrich, et al.Theorem Proving in Lean
[12]

Korn, Abhishek Parmar, Christina D

Ruoming Pang, Ramon Caceres, Mike Burrows, Zhifeng Chen, Pratik Dave, Nathan Germer, Alexander Golynski, Kevin Graney, Nina Kang, Lea Kissner, Jeffrey L. Korn, Abhishek Parmar, Christina D. Richards, and Mengzhi Wang. Zanzibar: Google’s consistent, global authoriza- tion syste...

2019
[13]

Accessed 31 May 2025

2024. Accessed 31 May 2025

2024
[14]

Ver- ifiable Credentials Data Model v2.1

Manu Sporny, Dave Longley, David Chaddwick, and Ivan Herman. Ver- ifiable Credentials Data Model v2.1. May 2025

2025
[15]

Egbert Rijke.Introduction to Homotopy Type Theory. 2022

2022
[16]

The Idris 2 Development Team.Idris 2 Tutorial. 2025. Accessed 31 May 2025

2025
[17]

eXtensible Access Control Markup Language (XACML) 3.0

OASIS XACML TC. eXtensible Access Control Markup Language (XACML) 3.0. January 2013

2013
[19]

Philip Wadler and Wen Kokke.Programming Language Foundations in Agda. 2023. Accessed 31 May 2025. 37

2023
[2024]

URLhttps://doi.org/10.1145/3649835. 36

doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

ALFA YAML Profile for XACML.https://alfa.guide

work page

[2] [2]

The Checker Framework.https://checkerframework.org/

work page

[3] [3]

openpolicyagent.org/docs/policy-language

Open Policy Agent — Rego Documentation.https://www. openpolicyagent.org/docs/policy-language

work page

[4] [4]

OpenFGA — Fine-grained Authorization.https://openfga.dev/

work page

[5] [5]

Ory – Open Source Identity Infrastructure.https://www.ory.sh/

work page

[6] [6]

Pydantic — Data Validation and Settings Management.https:// docs.pydantic.dev/latest/

work page

[7] [7]

HashiCorp Sentinel.https://www.hashicorp.com/sentinel

work page

[8] [8]

Styra Inc.https://www.styra.com/

work page