Lambda the Ultimate

Something can be versatile but incredibly slow to work with. I don't write machine code when a spreadsheet would do.

Certainly the learning curve for any of these tools is significant, particularly if you aren't already well-versed in whatever logic(s) underpin the tools. Beyond that, though, there tends not to be a royal road to programming language semantics: it never becomes easy; we're fortunate indeed when it becomes less hard.

So when I say "heavyweight," I'm thinking, in this case, about how long I feel it would reasonably take to formalize the definition of a DSL using one of these tools, and for any DSL other than one that was so trivial as to not be worth formalizing, I see such an effort requiring months—probably more than you would realistically have in a commercial setting, for better or for worse.

There is, of course, another approach, which is to express your DSL in terms of rewriting to another language that you can already reason about. This is the approach taken in Graydon Hoare's wonderful One-Day Compilers presentation, which essentially uses camlp4 (the O'Caml Pre-Processor and Pretty-Printer) and, of course, O'Caml, to do a source-to-source transformation from the DSL to C, and then compiles the C to generate the resulting program. The beauty of this approach is that thanks to camlp4's extensibility you can develop a DSL-to-X transformer, where "X" is anything you can write a custom printer similar to Hoare's Cquot for, and take advantage of all of O'Caml's semantics in doing so.

My sole goal is to reason about programs.

This is another goal entirely than stated in your original post.

By the time someone knows how to formalize a domain, or a language, in an interactive theorem prover my guess is that the burden of actually doing so becomes too big in a setting where money is to be made with a DSL. It's not about proving, it's about choosing the right design and your ability to choose the design right. Even for rapid prototyping I would first go for implementing prototypes in, well, rapid prototyping languages like Lisp, Haskell, or Python. Especially since formal proofs of algorithmic properties of programs are not interesting in most industrial settings; and I don't see formal rigorous development becoming cost-effective any time soon.

But if you want to learn/reason about programs, well, yeah, you could give Coq or Isabelle a spin (but be prepared for the rather steep learning curve).