AI systems increasingly synthesize executable structure at runtime: LLMs generate programs, agents construct workflows,self-improving systems modify their own behavior. In classical homoiconic and staged languages, the transition from coderepresentation to execution is unrestricted. eval is a language primitive, not a governed operation. We argue that ingovernedintelligent systems, this transition is an authority amplification: it converts symbolic structure into executableauthority andmust be mediated like any other effect. We present governed metaprogramming, a language design where programrepresentations(machine forms) are first-class values, form manipulation is pure computation, and materialization (the transition fromform toexecutable machine) is a governed effect subject to structural inspection. The governance system analyzes the proposedprogram'scapability requirements, policy compliance, and resource estimates before permitting execution. We formalize twojudgments: pureform evaluation (which emits no directives) and governed materialization (which emits exactly one governed directive). Weprovethree properties: purity of form manipulation, the no-bypass theorem, and boundary preservation. We implement the designinMashinTalk, a DSL for AI workflows compiling to BEAM bytecode, and report on integration with 454 existingmachine-checked Rocqtheorems. The central contribution is reclassifying eval from a language primitive into a governed effect.

翻译：人工智能系统日益在运行时合成可执行结构：大语言模型生成程序、智能体构建工作流、自改进系统修改自身行为。在经典的同像性和分阶段语言中，从代码表示到执行的转换是不受限制的。eval是一种语言原语，而非受管控的操作。我们论证，在受管控智能系统中，这种转换是一种权限放大：它将符号结构转换为可执行权限，必须像其他效应一样被中介处理。我们提出受管控元编程——一种语言设计，其中程序表示（机器形式）是一等值，形式操作是纯计算，而物化（从形式到可执行机器的转换）是一种受管控效应，需接受结构性审查。管控系统在允许执行之前，对所提议程序的能力需求、策略合规性和资源估计进行分析。我们形式化了两种判断：纯形式求值（不产生指令）和受管控物化（恰好产生一条受管控指令）。我们证明了三个性质：形式操作的纯度、无旁路定理和边界保持性。我们在MashinTalk中实现了该设计——一种编译到BEAM字节码的AI工作流领域特定语言，并报告了与454个现有机器验证的Rocq定理的集成情况。核心贡献在于将eval从一种语言原语重分类为一种受管控效应。