Galois has released a few well-documented examples including Ivory[1], a language for safer systems programming and Cryptol[2], a language for specifying cryptographic algorithms.

A couple of other low-level examples are Copilot[3] and Atom[4], both of which generate C for embedded programming but with somewhat different characteristics and aims.

On a slightly different note, we have SBV[5] (SMT-based verification) which presents a high-level programming model for using multiple SMT solvers including the recently open-sourced Z3.

All of these follow a pretty similar pattern in terms of letting you specify logic and generate code for it. A different sort of DSL can be found in various combinator libraries like Parsec[6] (for parsing) and the Wadler/Leijin Pretty Printer[7] for, well, pretty printing (ie the inverse of parsing).