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.

翻译：编程语言假设程序直接执行效果。当自主系统动态生成行为时，这一假设会出现问题：在决定行动与执行行动之间缺乏结构性的调节点。我们定义了意图驱动计算：一种编程模型，其中程序生成意图（描述提议行动的有限数据值），而非直接执行效果。受治理运行时将每个意图与可判定的策略语言进行比对，在防篡改账本中记录每一项决策，然后才实现该效果。该语言未提供通往效果的其他路径。该模型并不判定程序任意行为属性（根据莱斯定理，这不可能实现）。相反，它约束语言，使得所有产生效果的操作都被具体化为有限的意图值，从而将治理从程序语义的不可判定领域转移至意图数据的可判定领域。由此产生涌现特性：通过构造实现事件溯源、通过意图重放实现治理模拟、结构性审计完备性以及增强的人类可理解性。我们对该模型进行了形式化规约，在具体语言中实现并编译至BEAM虚拟机，并在Rocq中验证了关键性质（454条定理、36个模块、零条已接纳引理）。基于属性的测试（70,000+随机输入，零分歧）验证了实现与规约的一致性。