An experience report on writing usable DSLs in Coq
summary
A hardware DSL called koika is implemented as a deeply embedded AST in Coq with a few thousand lines of code and hundreds of lines of notations; usability comes from replacing Coq's parser with custom entries (Coq 8.9) so Gallina-like syntax inside double curly braces generates koika constructors and editor tooling still highlights and indents. An escape hatch via backticks mixes Gallina when needed. Identifier-to-string conversion uses Ltac2 to capture names without quotes, and a typeclass trick infers dependently typed membership proofs automatically; the libraries are a single short file and work in practice.
AI-written summary · about