> FWIW [...] Haskell

Sigh. So the wizziest Haskell programmer I know, has repeatedly done the following. They build a model of the mathematics of a problem domain. And then they mentally/manually compile that down to Haskell. Sometimes extending GHC internals to get an adequate target.

He's the compiler. It's a compilation process built of wizzy wet-ware, and Coq, and ... with very little tooling support. GHC is just the compiler target.

I'm not good enough to do that. I can't bridge that gap manually. That gap between insightful description of problem domain, and inexpressive language. I can't be the primary compiler, floating unsupported in air. I need a language and environment that has at least some clue what I'm trying to do. That participates and checks and supports me. That has a type system rich enough to directly describe problem domains, to describe math. Not merely a low-level target for a mental compiler.

Otherwise, everything I write is still just sculpting kludges.

GHC makes a nifty compiler target. All we need now, is a nifty compiler. ;)