Right! So you're trying to get ahold of the idea of an intelligent computational agent, in clear formalisms, and trying to solve the basic issues that arise there. And often, the issues you discover at the fundamental mathematical level work their way through to the highly applied level.

That makes sense. I feel like this is the most direct answer to the question

... are you curious why MIRI does so much with mathematical logic, and why people on Less Wrong keep referring to Löb's Theorem?