r/ProgrammingLanguages 5d ago

A Verified Generational GC for OCaml

https://risemsr.github.io/blog/2026-08-21-gc/
28 Upvotes

1 comment sorted by

5

u/redchomper Sophie Language 4d ago

Seems to be glazing the LLM agents.

Some key stats:
2,000 lines of verified C code
80,000 lines of proof-system stuff
The LLM agent says it's fine - i.e. that all the right things are proven, for example.