Thanks for the answer. I'm familiar with the "Impedance mismatch" that EDSL have in C++. If done right, it can be very limited. For example, I like what they did with NT2 (for Matlab programmer): https://www.lri.fr/~falcou/nt2/tutorial/matlab/first_example... . But it is not always possible, depending on the paradigm.

I agree that static analyses and invariant enforcement/extraction is a good reason to have a new language (I think most of the time you have to "get around" with "convention" when using C++ EDSL).