Verified Chester compiler (Coq/Rocq → OCaml → TypeScript / Go / Rocq).
Docs: guide · reference · paper — start at docs/README.md.
i really get a bit discouraged from trying this tool because its original name had dirty connotations. it is not pleasant when people mentioned its original name in english. but let's see..
Oh no this thing became another ai slop. Let's limit ai slop to implementations. Sementics shall be designed and understood by me