An experience report on writing usable DSLs in Coq
summary
A report on building a hardware DSL in Coq: the codebase totals a few thousand lines of Coq and hundreds of lines of notations; Coq 8.9 custom entries let the parser be replaced so Koika reuses Gallina syntax inside {{...}} and uses backticks as an escape hatch. Variable names auto-quote via ident_to_string and an ltac2 chain converts identifiers to strings; dependent AST indices resolve with a typeclass trick that synthesizes membership proofs, all packaged in a single short library.
AI-written summary · about