TIL that the CompCert verified C compiler is defined as a heavily documented literate program! So cool: compcert.org/doc/
Conversation
Hah, and I was already aware that CompCert was “quite the endeavor”. This just hammers it home even more. I'm glad this thing exists. 🥰
1
2
Show replies
Replying to
Is that a feature of compcert or just something they get for free by using coq?
1
I think it's more something from Coq, but it's not really for free, you still need to write the docs! There's also Alectron if you want even richer documentation generation for Coq:
1