Intent-Driven Computing: A Computational Model for Governed Autonomous Systems

Alan L. McCann

arxiv: 2605.24036 · v1 · pith:FDGK2QCEnew · submitted 2026-05-21 · 💻 cs.PL

Intent-Driven Computing: A Computational Model for Governed Autonomous Systems

Alan L. McCann This is my paper

Pith reviewed 2026-06-30 16:25 UTC · model grok-4.3

classification 💻 cs.PL

keywords intent-driven computinggoverned autonomous systemseffect reificationdecidable governanceevent sourcingaudit completenessprogramming modelpolicy enforcement

0 comments

The pith

Reifying all effects as finite intent values shifts governance of autonomous systems from undecidable semantics to decidable data.

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

The paper defines intent-driven computing as a model in which programs produce finite intent values describing proposed actions rather than executing effects directly. A runtime evaluates each intent against a decidable policy, records the decision in a tamper-evident ledger, and only then realizes the effect, with no other path to effects permitted. This constraint moves governance decisions into the domain of finite data, where they become decidable, and produces structural properties such as event sourcing by construction and complete audit trails. A sympathetic reader would care because autonomous systems that generate behavior dynamically have no reliable mediation point between decision and action under conventional models, and this approach addresses that gap without claiming to decide arbitrary behavioral properties.

Core claim

Intent-driven computing is defined by programs that produce only finite intent values, with a governed runtime that examines each intent against a decidable policy language, records every decision in a tamper-evident ledger, and realizes the effect only after approval. The language provides no alternative path to effects. By constraining the language so that every effectful interaction is reified as a finite intent value, governance shifts from the undecidable domain of program semantics to the decidable domain of intent data. This yields emergent properties including event sourcing by construction, governance simulation via intent replay, structural audit completeness, and improved human co

What carries the argument

Reification of every effectful action as a finite intent value, which moves all governance decisions onto decidable data.

If this is right

Event sourcing occurs automatically because every action begins as a recorded intent.
Governance policies can be tested by replaying recorded intents without executing live effects.
Audit completeness follows directly from the requirement that all effects pass through the ledger.
The approach applies only to properties decidable on finite data, consistent with Rice's theorem.
The implementation compiles to the BEAM virtual machine and matches the formal specification under extensive testing.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Systems built this way could support regulatory compliance checks performed entirely on ledger data.
Human operators might review proposed actions at the intent level before any runtime effect occurs.
The model could be adapted to other runtime environments beyond BEAM if the intent reification constraint is preserved.
Intent replay might allow offline simulation of governance outcomes for policy refinement.

Load-bearing premise

Every possible effectful action in an autonomous system can be represented as a finite intent value without unacceptable loss of expressiveness or functionality.

What would settle it

An autonomous system action whose necessary effect cannot be captured by any finite data value without losing required behavior or expressiveness.

Figures

Figures reproduced from arXiv: 2605.24036 by Alan L. McCann.

**Figure 2.** Figure 2: Operational semantics pipeline. A program term evaluates to an [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

read the original abstract

Programming languages assume programs directly execute effects. When autonomous systems generate behavior dynamically, this assumption becomes problematic: there is no structural mediation point between deciding to act and acting. We define intent-driven computing: a programming model where programs produce intents (finite data values describing proposed actions) rather than directly executing effects. A governed runtime examines each intent against a decidable policy language, records every decision in a tamper-evident ledger, and only then realizes the effect. The language provides no alternative path to effects. The model does not decide arbitrary behavioral properties of programs (which Rice's theorem shows is impossible). Instead, it constrains the language so that all effectful interaction is reified as finite intent values, shifting governance from the undecidable domain of program semantics to the decidable domain of intent data. This yields emergent properties: event sourcing by construction, governance simulation via intent replay, structural audit completeness, and improved human comprehensibility. We specify the model formally, implement it in a concrete language compiling to the BEAM virtual machine, and verify key properties in Rocq (454 theorems, 36 modules, zero admitted lemmas). Property-based testing (70,000+ random inputs, zero disagreements) validates that the implementation matches the specification.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper defines a model forcing effects through finite intents for decidable governance, with solid Rocq verification backing the core mechanics.

read the letter

The main thing to know is that this work reifies all program effects as finite intent data values, so a governed runtime can check them against policies before any action happens, with everything logged to a tamper-evident ledger. This is implemented as a concrete language compiling to BEAM, and the authors supply 454 Rocq theorems with zero admits plus 70,000+ property tests with zero failures.

What the paper does well is make the shift from undecidable program semantics to decidable intent data explicit and machine-checked. The handling of Rice's theorem is direct: they do not claim to decide arbitrary behaviors but instead constrain the language so effects must go through intents. That produces the claimed emergent properties like built-in event sourcing and replay-based simulation. The verification effort is real evidence the model is consistent as defined.

The soft spot is the central modeling choice that every effectful action in autonomous systems can be represented as finite intent values without unacceptable loss of functionality. The abstract flags that the model does not decide behavioral properties, which is fair, but the practical trade-off in expressiveness for dynamic autonomous behavior gets less concrete treatment.

This is for programming-language and systems researchers working on policy-enforced autonomy. The formal grounding is strong enough that it deserves a serious referee even if revisions are needed on the expressiveness question.

Referee Report

0 major / 2 minor

Summary. The paper defines intent-driven computing as a programming model in which programs produce finite intent data values describing proposed actions instead of directly executing effects. A governed runtime evaluates each intent against a decidable policy, records the decision in a tamper-evident ledger, and only then realizes the effect. The model is specified formally, implemented in a language targeting the BEAM virtual machine, and key properties are verified in Rocq with 454 theorems across 36 modules (zero admitted lemmas) and validated with over 70,000 property-based tests (zero disagreements). It claims to shift governance to the decidable domain of intent data, yielding properties such as event sourcing by construction and structural audit completeness.

Significance. If the central claim holds, this work is significant for programming language design in autonomous systems, as it provides a structural way to make governance decidable without violating Rice's theorem by constraining the language to intent-based effects. The extensive machine-checked verification and property testing are notable strengths that lend credibility to the realizability of the model and its emergent properties.

minor comments (2)

[Abstract] Abstract: the sentence beginning 'The model does not decide arbitrary behavioral properties' could be clarified by explicitly cross-referencing the section that states the language constraint (no alternative path to effects) to avoid any implication that the model attempts undecidable checks.
The verification claims (454 theorems, 36 modules) are strong but would benefit from a brief table or list in the verification section enumerating the main properties proved (e.g., intent-only effects, ledger tamper-evidence) to make the machine-checked results more immediately usable by readers.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and the recommendation to accept. The summary accurately captures the core model, formal verification, and emergent properties.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper defines a language constraint that reifies effects as finite intents, then verifies the resulting decidability and emergent properties (event sourcing, audit completeness) via an independent Rocq formalization (454 theorems, zero admitted lemmas) and property-based testing on 70k+ inputs with zero disagreements. No equations reduce results to fitted parameters or self-referential definitions; the 'by construction' properties are explicitly stated as consequences of the language restriction rather than derived predictions. The central claim does not rely on self-citations or imported uniqueness theorems. The derivation chain is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Abstract-only review; no explicit free parameters, axioms, or invented entities beyond the core model concepts can be extracted. The model itself introduces 'intents' and 'governed runtime' as central constructs.

axioms (1)

standard math Rice's theorem establishes that arbitrary behavioral properties of programs are undecidable.
Invoked explicitly to justify why the model does not attempt full semantic analysis.

invented entities (1)

intent (finite data value describing proposed action) no independent evidence
purpose: Reify all effectful operations so they become checkable data rather than direct execution.
Central to the model; no independent evidence outside the paper is provided in the abstract.

pith-pipeline@v0.9.1-grok · 5739 in / 1404 out tokens · 22756 ms · 2026-06-30T16:25:33.759393+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

15 extracted references · 14 canonical work pages · 2 internal anchors

[1]

doi: 10.1109/LICS.2003.1210062. James P. Anderson. Computer security technology planning study. InTechnical Report ESD-TR- 73-51,

work page doi:10.1109/lics.2003.1210062 2003
[2]

Constitutional AI: Harmlessness from AI Feedback

Yuntao Bai, Saurav Kadavath, Sandipan Kundu, Amanda Askell, Jackson Kernion, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, et al. Constitutional AI: Harmlessness from AI feedback.arXiv preprint arXiv:2212.08073,

work page internal anchor Pith review Pith/arXiv arXiv
[3]

doi: 10.1016/j.jlamp.2014. 02.001. Peter Buneman, Sanjeev Khanna, and Wang-Chiew Tan. Why and where: A characterization of data provenance. pages 316–330,

work page doi:10.1016/j.jlamp.2014 2014
[4]

doi: 10.1007/3-540-44503-X

work page doi:10.1007/3-540-44503-x
[5]

doi: 10.1145/2898442.2898444. Jack B. Dennis and Earl C. Van Horn. Programming semantics for multiprogrammed computations. Communications of the ACM, 9(3):143–155,

work page doi:10.1145/2898442.2898444
[6]

Martin Fowler

doi: 10.1145/365230.365252. Martin Fowler. Event sourcing. https://martinfowler.com/eaaDev/EventSourcing.html,

work page doi:10.1145/365230.365252
[7]

Oleg Kiselyov and Hiromi Ishii

doi: 10.1145/3062341.3062363. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. InProceedings of the 2015 ACM SIGPLAN Symposium on Haskell, pages 94–105,

work page doi:10.1145/3062341.3062363 2015
[8]

Ben Laurie, Adam Langley, and Emilia K¨ asper

doi: 10.1145/2804302.2804319. Ben Laurie, Adam Langley, and Emilia K¨ asper. Certificate transparency. InRFC 6962,

work page doi:10.1145/2804302.2804319
[9]

Martin Leucker and Christian Schallhart

doi: 10.1145/3009837.3009872. Martin Leucker and Christian Schallhart. A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 78(5):293–303,

work page doi:10.1145/3009837.3009872
[10]

Paul Blain Levy.Call-By-Push-Value: A Functional/Imperative Synthesis

doi: 10.1016/j.jlap.2008.08.004. Paul Blain Levy.Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation. Springer,

work page doi:10.1016/j.jlap.2008.08.004 2008
[11]

doi: 10.1007/978-94-007-0954-6. Alan L. McCann. Effect-transparent governance for AI workflow architectures: Semantic preservation, expressive minimality, and decidability boundaries.arXiv preprint arXiv:2605.01030, 2026a. Alan L. McCann. Mechanized foundations of structural governance: Machine-checked proofs for governed intelligence.arXiv preprint arXiv...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1007/978-94-007-0954-6
[12]

Handlers of algebraic effects

Gordon Plotkin and Matija Pretnar. Handlers of algebraic effects. InProgramming Languages and Systems (ESOP 2009), volume 5502 ofLNCS, pages 80–94. Springer,

2009
[13]

Nemo guardrails: A toolkit for controllable and safe LLM applications with programmable rails.arXiv preprint arXiv:2310.10501,

Traian Rebedea, Razvan Dinu, Makesh Sreedhar, Christopher Parisien, and Jonathan Cohen. Nemo guardrails: A toolkit for controllable and safe LLM applications with programmable rails.arXiv preprint arXiv:2310.10501,

work page arXiv
[14]

Andrei Sabelfeld and Andrew C

doi: 10.2307/1990888. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security.IEEE Journal on Selected Areas in Communications, 21(1):5–19,

work page doi:10.2307/1990888
[15]

doi: 10.1109/JSAC.2002.806121. 18

work page doi:10.1109/jsac.2002.806121 2002

[1] [1]

doi: 10.1109/LICS.2003.1210062. James P. Anderson. Computer security technology planning study. InTechnical Report ESD-TR- 73-51,

work page doi:10.1109/lics.2003.1210062 2003

[2] [2]

Constitutional AI: Harmlessness from AI Feedback

Yuntao Bai, Saurav Kadavath, Sandipan Kundu, Amanda Askell, Jackson Kernion, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, et al. Constitutional AI: Harmlessness from AI feedback.arXiv preprint arXiv:2212.08073,

work page internal anchor Pith review Pith/arXiv arXiv

[3] [3]

doi: 10.1016/j.jlamp.2014. 02.001. Peter Buneman, Sanjeev Khanna, and Wang-Chiew Tan. Why and where: A characterization of data provenance. pages 316–330,

work page doi:10.1016/j.jlamp.2014 2014

[4] [4]

doi: 10.1007/3-540-44503-X

work page doi:10.1007/3-540-44503-x

[5] [5]

doi: 10.1145/2898442.2898444. Jack B. Dennis and Earl C. Van Horn. Programming semantics for multiprogrammed computations. Communications of the ACM, 9(3):143–155,

work page doi:10.1145/2898442.2898444

[6] [6]

Martin Fowler

doi: 10.1145/365230.365252. Martin Fowler. Event sourcing. https://martinfowler.com/eaaDev/EventSourcing.html,

work page doi:10.1145/365230.365252

[7] [7]

Oleg Kiselyov and Hiromi Ishii

doi: 10.1145/3062341.3062363. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. InProceedings of the 2015 ACM SIGPLAN Symposium on Haskell, pages 94–105,

work page doi:10.1145/3062341.3062363 2015

[8] [8]

Ben Laurie, Adam Langley, and Emilia K¨ asper

doi: 10.1145/2804302.2804319. Ben Laurie, Adam Langley, and Emilia K¨ asper. Certificate transparency. InRFC 6962,

work page doi:10.1145/2804302.2804319

[9] [9]

Martin Leucker and Christian Schallhart

doi: 10.1145/3009837.3009872. Martin Leucker and Christian Schallhart. A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 78(5):293–303,

work page doi:10.1145/3009837.3009872

[10] [10]

Paul Blain Levy.Call-By-Push-Value: A Functional/Imperative Synthesis

doi: 10.1016/j.jlap.2008.08.004. Paul Blain Levy.Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation. Springer,

work page doi:10.1016/j.jlap.2008.08.004 2008

[11] [11]

doi: 10.1007/978-94-007-0954-6. Alan L. McCann. Effect-transparent governance for AI workflow architectures: Semantic preservation, expressive minimality, and decidability boundaries.arXiv preprint arXiv:2605.01030, 2026a. Alan L. McCann. Mechanized foundations of structural governance: Machine-checked proofs for governed intelligence.arXiv preprint arXiv...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1007/978-94-007-0954-6

[12] [12]

Handlers of algebraic effects

Gordon Plotkin and Matija Pretnar. Handlers of algebraic effects. InProgramming Languages and Systems (ESOP 2009), volume 5502 ofLNCS, pages 80–94. Springer,

2009

[13] [13]

Nemo guardrails: A toolkit for controllable and safe LLM applications with programmable rails.arXiv preprint arXiv:2310.10501,

Traian Rebedea, Razvan Dinu, Makesh Sreedhar, Christopher Parisien, and Jonathan Cohen. Nemo guardrails: A toolkit for controllable and safe LLM applications with programmable rails.arXiv preprint arXiv:2310.10501,

work page arXiv

[14] [14]

Andrei Sabelfeld and Andrew C

doi: 10.2307/1990888. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security.IEEE Journal on Selected Areas in Communications, 21(1):5–19,

work page doi:10.2307/1990888

[15] [15]

doi: 10.1109/JSAC.2002.806121. 18

work page doi:10.1109/jsac.2002.806121 2002