I'd totally use a memory safe browser even if it made all the C++ code 4x slower. Execution time of C++ code is far from a bottleneck in the perceived speed of a web browser these days. I guess the main downside would be the lack of a JIT for JavaScript. Would it ever be possible to extend Fil-C's safety guarantees to a JIT compiler? I'm not sure how that would work.
I’ve thought about the JIT a lot. JSC’s JITs are dear to my heart :-)
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 :-)
I'd totally use a memory safe browser even if it made all the C++ code 4x slower. Execution time of C++ code is far from a bottleneck in the perceived speed of a web browser these days. I guess the main downside would be the lack of a JIT for JavaScript. Would it ever be possible to extend Fil-C's safety guarantees to a JIT compiler? I'm not sure how that would work.
I’ve thought about the JIT a lot. JSC’s JITs are dear to my heart :-)
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 :-)
Me too!