I'm posting this from a memory safe web browser
Hi everyone! I'm posting this from a memory safe browser: WebKitGTK MiniBrowser compiled with Fil-C, plus all dependencies compiled with Fil-C
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. 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 :-)