Still dealing with a tail of bugs, some of which look like overzealous optimizations leading to loss of pointer capability (leading to a filc panic). But it works well enough that I can say "hi" on here.
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 :-)