I've had a lot of luck with little languages that have an escape hatch into the implementation language. My "little languages" always have atomic programs/expr

I've had a lot of luck with little languages that have an escape hatch into the implementation language. My "little languages" always have atomic programs/expressions whose meaning is given by an implementation in the base language. Sometimes, e.g., when my little language has an optimizing compiler or some fancy semantics, the atomic programs/expressions need a tighter interface than "does something". In those cases, I write down the full semantics of the language and figure out what lemmas I need to prove about atomic programs/expressions in order to prove whatever property I want about the overall language. I then enforce those lemmas at runtime using asserts (or, in the case of termination, wrapper code that enforces a timeout). This pretty much only goes wrong when "everything" is factored out into the atomic programs/expressions. I avoid these situations by only using "little languages" when I can do something useful and difficult using the semantics of the little language. Most common examples include: automatic optimization, automatic parallelization, and automatic verification/static analysis. But even when it does go wrong in this way, it's no the end of the world: if everything is implemented in the atomics, then you just refactor the implementations of the atomic programs/expressions into a library, delete the interpreter/compiler, and write some wrapper code.