I found this interesting post over at lambda the ultimate about constructing a provably total (terminating) self-compiler. It looked quite similar to some of the stuff MIRI has been doing with the Tiling Agents thing. Maybe someone with more math background can check it out and see if there are any ideas to be shared?
This is the same basic idea as Benja's Parametric Polymorphism, with N in the post corresponding to kappa from parametric polymorphism.
The "superstition" is:
...We make our compiler superstitious as follows: we pick an unused no-op of the target machine that should never occur in normal generated code and add an axiom that says that running this no-op actually bumps a counter that exists in the ether, and, if this unseen counter exceeds N, then it halts execution of the machine. Since we could have started with an arbitrary N, we will never reach a
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.