What is the 'tower of interpreters'?	The stack of layers between a program's meaning and the matter that runs it: math spec → program → ISA → microarchitecture → RTL/gates → transistors → device physics. Each layer is one interpreter standing on another, and each charges its own interpretation tax.
In this framing, what is hardware specialization?	Collapsing levels of the tower. Every level you collapse — by proving enough about the program to bake it into the layer below — is interpretation overhead deleted permanently. Native compilation collapses the top two rungs; a custom circuit collapses most of them; analog compilation collapses the lot.
Why is a general-purpose CPU the most *expensive* interpreter ever built?	Precisely because it's general. On every instruction it fetches, decodes, renames registers, predicts branches, and routes operands through a datapath wide enough for any program — none of which computes your answer. It's the tax you pay, billions of times, for the flexibility to run any program.
Does the machine-checked guarantee survive the descent into hardware?	Yes, down to RTL and FPGAs today. The correctness statement is invariant: lower(p) ⊑ p — the artifact one rung down refines the meaning one rung up. Stack the refinements (CakeML→Silver, Lutsig, Kami) and you get an end-to-end theorem from source semantics to gate-level netlist, each link kernel-checked.