2 ms·
A mechanically verified garbage collector for OCaml [pdf]
- Ecco 2y agoWhat are those numbers on the sides for?
- codelion 2y agoI think it is preprint, some latex templates put the numbers to make it easy for reviewers to refer them.
- yawaramin 2y agoSomething very cool about this GC is that it's written in F* (technically, a low-level subset called Low) and compiles to memory-safe C,* so it's kind of equivalent to using Rust but they don't have to give up C. F/Low are also used in Project Everest, which ships formally verified crypto primitives in Firefox and other platforms.
- a-french-anon 2y agoI don't want to rain on such a cool parade, but I'm pretty sure doing the same with a truly performant GC is a whole different ballgame.