Speaker: Liron Cohen

Title

The Effects of Effects on Constructivism

Abstract

Constructivism begins with the promise that truth has computational meaning. Yet our standard picture of constructive validity grew out of a pure model of computation, inherited from the lambda calculus. Is this purity a foundational necessity, or merely a historical convenience? Today, computation is effectful: programs store state, branch nondeterministically, raise exceptions, interact with environments, sample randomly, and manipulate continuations. If constructive foundations are meant to explain computation, rather than idealize it away, then effects must move from the margins into the logical core. In this talk, I will argue that effects are not obstacles to constructivism. They are the structure that a modern constructivism should be built from. Once effects are admitted, they reshape the validity of logical principles: sometimes breaking them, sometimes restoring them, and often revealing distinctions that pure foundations hide. I will illustrate this through examples involving choice, continuity, and Markov’s principle. What emerges is not a weaker constructivism, but a more honest one: a constructivism whose logical principles are grounded in the actual structure of computation.