You probably need a programming language more powerful than Rust that can encode and check the complicated invariants needed by the JIT.
There are classes of type system—"dependently-typed"—where you can encode arbitrary predicates into the type checking. I've remember seeing examples where they could prove arbitrary facts at the assembly level, including self-modifying code. Lean is such a language, currently very popular, but there are others.
Correctness of such programs depends on some basic assumptions about the CPU/memory environment, which should work absent hardware bugs like speculative execution or side channels. Although these could probably be encoded as well, and accounted for.
Without such a general proof language, you could probably make a special language to support JIT development, although its type system would be very complicated and the language itself could be a source of bugs.
Given such languages or proofs (maybe tractable now with AI-assisted theorem proving), you can actually make insanely performant code, since you don't really need to rely on other runtime protection so much (although maybe a good idea still).
There are classes of type system—"dependently-typed"—where you can encode arbitrary predicates into the type checking. I've remember seeing examples where they could prove arbitrary facts at the assembly level, including self-modifying code. Lean is such a language, currently very popular, but there are others.
Correctness of such programs depends on some basic assumptions about the CPU/memory environment, which should work absent hardware bugs like speculative execution or side channels. Although these could probably be encoded as well, and accounted for.
Without such a general proof language, you could probably make a special language to support JIT development, although its type system would be very complicated and the language itself could be a source of bugs.
Given such languages or proofs (maybe tractable now with AI-assisted theorem proving), you can actually make insanely performant code, since you don't really need to rely on other runtime protection so much (although maybe a good idea still).