Best idea so far is that Fil-C exposes an abstract and memory safe JIT API that severely restricts what you can do and pessimizes codegen but enforces the Fil-C capability model in some kind of easily validated way.

You could imagine then growing the power of that API and adding optimizations while maintaining a proof of correctness in Lean or Rocq or whatever.

I think where it ends is something that looks like PCC if you squint:

- JSC JITs would generate abstract machine code via an API while also making calls that provide proofs that Fil-C checks are not needed

- Fil-C runtime converts the abstract machine code to actual machine code while checking the proof

- The proof checker is itself proved correct in lean or rocq

Sounds like a lot of work to get there. Also, sounds like a very fun thing to build :-)