>A toolkit where you can create DSLs with limited expressiveness, which in turn make it easy to build and verify things. This is a common approach in the Coq e

>A toolkit where you can create DSLs with limited expressiveness, which in turn make it easy to build and verify things. This is a common approach in the Coq ecosystem, writing DSls for building things, and custom automation for them. See for instance papers by Adam Chlipala.