logoalt Hacker News

genxyyesterday at 1:51 PM2 repliesview on HN

If we are sprinkling formal verification on things, we can sprinkle it on a JIT.


Replies

bastawhizyesterday at 2:30 PM

But then we'd have to admit that it's not the JIT that's a problem, it's the lack of guardrails and analysis features in the machine code interfaces that higher level languages expose!

pjmlpyesterday at 5:55 PM

Only if it goes through verified bytecode, and the set of instructions is provable.

The JIT must also only be allowed to call into specific code, controlled by the runtime, and nothing else.