Hacker News Reader

I think it makes more sense to verify that the jit is correct than to verify that it's output is correct at runtime.

Nah

It's damn near impossible to verify that the JIT is correct.

But it is possible to verify at runtime that the code that the JIT emitted obeys some memory safety law.

(V8's heap sandbox is an example of this; a sarcastic JIT would be an arguably stronger example of this.)

If you have a runtime check of some correctness, why can't you just prove that the output of your compiler always passes that check?

One might argue that verifying the correctness of a JIT is basically the same problem as verifying the correctness of an entire compiler, with the added caveat that malicious inputs to the JIT are expected whereas malicious inputs to a compiler might be seen as rare.

IIRC rustc still has a couple of known soundness bugs, for example. It’s only been a few weeks since someone managed to exploit Lean, and Lean is all about formalizing things :)

Reply on news.ycombinator.com