Why I Study Foundations
A reflection on the pull of mathematical logic and the foundations of computation — and why these questions feel more urgent than ever.
People ask me why I would choose to study something as abstract as the foundations of computation. Isn’t that all settled? Didn’t Turing and Gödel close the book on this in the 1930s?
I never know quite how to answer. The honest reply is that the questions haven’t changed — we just have more language to ask them badly.
When I first read about the Halting Problem, I was struck not by the impossibility result itself but by the method of proof. Turing’s diagonal argument is not exotic machinery; it is a kind of philosophical judo, turning a system’s own expressiveness against itself. The same structure underlies Gödel’s incompleteness, Cantor’s theorem, Russell’s paradox. There is something here that keeps recurring, a pattern that lives beneath the mathematics.
That pattern interests me more than any particular theorem.
The question I keep returning to is this: what does it mean for a system to understand itself?
This is not mysticism. It is a precise question in the theory of computation. And the answer — that sufficiently powerful systems cannot fully introspect without contradiction — has consequences that feel far from abstract in 2025, when we are building systems with enormous capability and very little principled understanding of what they are doing.
I do not think foundations will directly solve the alignment problem or make language models more interpretable. But I think the conceptual tools we build in logic and type theory are part of the vocabulary we will need. Proof assistants, formal verification, dependent types — these are already moving from pure theory into engineering practice.
There is also something simpler. Mathematics at the foundational level is beautiful in a way that feels different from applied work. Not superior — just different. A proof that a certain class of functions is not computable does not help anyone build a faster sorting algorithm. But it draws a clean boundary around what is possible, and there is a satisfaction in that clarity that I find nowhere else.
This is probably not a compelling career pitch. But it is the honest one.