AI summaryⓘ
The authors introduce ETAS, a programming language designed to help build agents that can interact with tools, handle approvals, and keep track of their actions in a clear and structured way. Unlike usual languages, ETAS treats elements like memory, prompts, and policies as fundamental parts of the program, separating predictable computation from unpredictable agent behavior. They created rules to check types and trace the agent's actions to ensure safety and correctness. The authors also built ETAS in Rust, providing tools to monitor and verify agent activities during execution, aiming to support reasoning about permissions, decisions, and audits. This approach helps programmers better understand and control what agents do and why.
agent systemstype systemseffect systemsauthorizationcompile-time checksexecution tracespolicy enforcementnondeterminismRust programming languageruntime monitoring
Authors
Huiri Tan, Yikun Wang, Puyang Zhang, Shangyu Li, Jiasi Shen
Abstract
ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic nondeterminism and externally visible actions while preserving a direct programming style. We present the core design of ETAS. Its static semantics assigns ordinary types through spec conformance and tracks each computation with two behavioral indices: an escaping effect row and a persistent abstraction of the typed action trace it may request. Specs form a terminating compile-time constraint calculus: type specs provide evidence for polymorphism and resource facts, callable specs constrain function and stage shapes, and trace specs express allow, deny, and temporal constraints. Typing checks requested traces against compiled monitors and emits residual obligations when dynamic resources preclude a complete static proof. The dynamic semantics distinguish requested, handled, denied, and committed events; handlers interpret typed actions without making their requests invisible to authorization or audit. We formalize a core calculus and state preservation, progress, type/effect soundness, handler trace-transparency, and policy safety. We also implement ETAS in Rust with a command-line interface, typed HIR checks, effect and policy diagnostics, handler checks, and trace-aware execution hooks. ETAS provides a programming-language foundation for reasoning about authorization, nondeterminism, recovery, and audit evidence before and during agent execution.