All the time, and BTW, I didn't say JITs sacrifice soundness but that they don't require proof of soundness. That's different as I'll show. Let me give you two

All the time, and BTW, I didn't say JITs sacrifice soundness but that they don't require proof of soundness. That's different as I'll show. Let me give you two common examples: virtual calls and branches. A JIT will speculatively devirtualize and inline a virtual call at a particular callsite if it has only encountered one or a small number of concrete instances, even if it can't prove that those are the only instances that can be encountered at that callsite. This is still sound because the JIT will emit a trap that will trigger if an unknown target is ever encountered, in which case it will deoptimize the compilation, go back to the interpreter and then compile again under new assumptions. Another example is branch elimination. If a JIT only ever encounters the program taking one side of a branch, it will only compile that branch (and introduce a trap), even if it can't prove that only that side will ever be taken.