Session Description

Naur’s programming as theory building (1985) suggests that programmers of an artifact keep in their mind a theory of the artifact, one that can guide its evolution. Without that theory, it is hard to keep the integrity of the program as it evolves.

With AI, who keeps that theory? As humans, we still want ownership, control, and understanding, to guide the evolution of the system and use it properly, even if the AI has generated it. Is the solution to try to write more of this “theory” in ways that can be accounted for? The ultimate accounting is checkable code. With AI, we need more ways for accounting but we can also now get them (including all the semi-formal ways).

I think verification is a step in the right direction, but we need even higher level sanity checks, and we also need to know which verified statements are important or incidental. The way we deal with ambiguity can guide which decisions we record and deliberately make. Finally, we need to think about verification/checking for systems, with ground truths in code, rather than just about our code artifacts.

I present some examples in LemmaScript (a verification toolchain for TypeScript developed by my startup Midspiral), Djinnlang (an unambiguous specification language with an LLM compiler developed by PhD student Simon Henniger), and Guardians of the Agents (a CACM 2026 article by Erik Meijer, which inspired me to do a prototype).