[hovav]

A JIT is a machine for turning logic bugs into memory unsafety. Rewriting a JIT in Rust won't eliminate logic bugs and won't guarantee memory safety for the binary output of the JIT (as distinct from the JIT implementation itself).

[infogulch]

Agreed. But the way you put it makes me wonder how many memory safety vulns have been found in JIT implementations (not the machine code they output).

[nextaccountic]

Okay, but in this case software verification like with Coq or F* could help

[hovav]

Yes! See, e.g., Fraser Brown et al., "Towards a Verified Range Analysis for JavaScript JITs," in proc. PLDI 2020, https://www.cs.utexas.edu/~hovav/dist/vera.pdf