I'm getting serious about decision theory. I have some foundational observations, upon which I'm building a mathematical framework. I have some partial drafts, and plan to write papers on it.

Most problems in decision theory are the result of insufficient rigor. "Rigor" to me means formalizing problems fully and proving things about the formalization, without use of fuzzy language. Full formalization means writing out the problem statement as two type-checkable functions, a world function which maps strategies to outcomes and a preference function which defines an ordering over outcomes. To my knowledge, none of the decision theory in the literature is done at this level of rigor. I have chosen a subset of SML/NJ, extended to include limiting expressions, as the representation for formalized problems, because it has solid mathematical foundations with which I am already familiar, and also a rigorous model of partial evaluation.

There is a pre-existing body of work on how to prove things about programs and transform and simplify them in provably correct ways in computer science: compiler theory. One of the major themes I've picked up from studying compilers is that different representations enable us to prove different things and perform different operations. In practice every compiler takes programs through a long series of intermediate representations. One of these representations, Static Single-Assignment (SSA) form, is strongly analogous to Pearl's causal models. Another representation, continuation-passing style (CPS), enables a natural and precise statement of one interpretation of causal decision theory, along with a precise description of when it does and doesn't work, such that you could prove that CDT is valid for a particular problem as a lemma and then apply CDT to it.

I haven't proved it yet, but I think I can prove within the framework I've defined that Eliezer's answer to the Prisoner's Dilemma, "cooperate iff your opponent cooperates iff you cooperate", is uncomputable, and that there is an infinite series of successively better approximations such that the Prisoner's Dilemma has no optimal answer.