In Code They Act, In Proof We Trust — Erik Meijer, Leibniz Labs
Erik Meijer argues that LLMs with tool calls are intrinsically dangerous because their agentic loop can produce irreversible side effects, and proposes that safety requires proof-carrying code: the model should output a symbolic plan (a free monad expression) rather than executing effects directly. This plan can be statically analysed for safety before any side-effectful execution occurs, reviving 1990s proof-carrying code concepts.