In one line, what is a compiler optimization?	Runtime work you proved you don't have to do. Every classical optimization is a static fact plus the runtime work that fact makes redundant — constant folding needs a singleton, dead-branch elimination needs an always-false guard, bounds-check elimination needs an interval containment.
Is abstract interpretation the same as 'compiling by proving'?	Almost — they're the two halves. Abstract interpretation proves a *property* (an over-approximation: reachable ⊆ γ(a)); compiling-by-proving / partial evaluation proves an *equivalence* (this fast residual = running the interpreter). AI produces facts; the second half cashes them into faster, semantics-preserving code.
What is the 'hinge' that turns an analysis into a compiler?	A precise-enough over-approximation becomes an equivalence. If the interval domain proves the top of stack is the singleton {0}, the abstraction has collapsed to a point — folding [push k, add] → [push k] is no longer merely licensed, it's forced. Precision, not soundness, is what deletes work.
Why is 'soundness is free, precision is expensive' the load-bearing caveat?	You can always prove a sound-but-useless invariant (⊤ everywhere) — it licenses nothing. Optimization power is bounded by precision, which is the undecidable, open-ended part. 'Prove more' must mean 'prove more singletons, unreachability, and no-overflow facts,' not 'prove more theorems.'