I wanted to share this primarily because I really enjoy how, as a matter of dovetailing, the interviewee outlines exactly the categorical structures present in Turing categories.
At 6:45 or so, we have an informal string diagram. On the left is the (Turing) category of source texts in H, and on the right is the (Turing) category of executables in B’. We’d like to imagine that we can send our tombstones, which are each arrows, from H to B’. How can we do that?
At 10:00 or so, we have a way to send objects and arrows from H to B’ in a way which we hope will commute. The commuting conditions are explained over the next couple minutes. These bootstrapping compilers are functors from H to B’. But note that they are also arrows in B’. This means that B’ can represent functors into itself.
Because B’ can represent functors into itself, it would turn out that we’re really talking about a structure which encompasses B’ and H. And also anything else which is Turing-equivalent, leading to an ∞-category Tomb whose objects are towers of compilers.
I find it delightful that the pattern of compilers from X to Y written in Y recurs throughout the video, as these are precisely the functors from X to Y in Tomb.
At 21:00 or so, there is an understanding that choosing an intermediate code is like finding a higher-level analogue of a Turing object. I don’t have a strong intuition for this yet, and can’t explain it.