Fwiw, I agree about supercompilation. Some have noted that JIT systems perform many of the same things as supercompilation, and it seems reasonable to consider

Fwiw, I agree about supercompilation. Some have noted that JIT systems perform many of the same things as supercompilation, and it seems reasonable to consider that JIT is part of the equation for optimising performance when systems are pushed to production. We've been doing that for decades now, with increasing sophistication in the details. Profile driven, multiple stages of specialisation and optimisation. Not quite to the levels of proof systems (and therefore supercompilation as envisioned) yet - there's plenty of room to get better at it - and we need to go there if we want those "zero cost abstractions" across modules that aren't designed for it, often with significant impedance mismatches.