There aren't any, that's the problem. Because most language designers these days seem to think that the best way to solve problem X is to develop an entire closed-garden ecosystem that also can solve Y and Z, and ends up doing none of them well, while forcing you to use their language and only their language.
Everywhere I've worked, I have seen the same things reimplemented poorly over and over again in general-purpose languages. Every system I've worked on is roughly a mash-up of database, dataflow graph, state machine, work scheduler, IPC, process coordination, programming in the large, and very low-level algorithmic stuff. Each of these could be factored out into a common simple language, but almost invariably they're just patterns imposed on C/C++/Java/what-have-you code. This greatly hampers understanding and analyzability.
There are rare occasions I see DSLs used to fulfill these roles, and it's to great benefit. Working with a well-designed PostgreSQL database rather than some half-baked home-grown object database is a dream. You get a concurrency model that works, and you can extract graphs of your data model for free. Same with using a state machine description language like SMC rather than hand-coding stuff as C++ boilerplate. Same with using a process coordinator like Erlang's OTP (which isn't a DSL but is close enough).
I'm not writing these posts to try to get developers to use DSLs more often. I'm writing them to try to get language designers to design DSLs more often.
On Coq:
Coq is not at all a practical programming language, since it has no concept of communication with external processes (i.e. I/O). This is exactly as it should be, since Coq is focused precisely on the domain of functional algorithms (and proofs). And, I have found that, within that domain, the restriction that all my algorithms must provably terminate is nearly invisible.
There is a very simple general way to ensure that all programs in Coq terminate: augment each recursive function with one additional argument which is a counter which must always count down to 0 (at which point recursion must halt). On the initial call to a recursive function, select a starting value for this counter which is greater than the number of iterations the algorithm requires. (When proving correctness in Coq, you will be asked to prove that this starting value is in fact suitably high.)
I have kept this requirement in mind when designing programs in other languages, and I have found it trivial to meet in all cases. Turing-completeness is not a feature I need in a programming language.
"I'm not writing these posts to try to get developers to use DSLs more often. I'm writing them to try to get language designers to design DSLs more often."
I was actually baiting you to blast you given I guessed the answer to number 1. However, I decided against it since you have the more reasonable position of identifying the problem then pushing responsibility onto language designers rather than users. Many posts seem other way around. So, that's refreshing. :)
"There are rare occasions I see DSLs used to fulfill these roles, and it's to great benefit."
I agree. iMatix, REBOL/RED, and LISP community (esp Racket) have shown it consistently in terms of productivity and reliability with performance being better sometimes. True even for general-purpose, systems programming: see Ivory langauge from Galois.
"SMC rather than hand-coding stuff as C++ boilerplate. Same with using a process coordinator like Erlang's OTP (which isn't a DSL but is close enough)."
OTP as a coordinator DSL I haven't thought about. Might look into it to see if there's design wisdom to learn for a future DSL outside of Erlang.
"I'm writing them to try to get language designers to design DSLs more often."
I know there's been some good books and essays on how to best design DSL's. Most of us don't know which ones are the good ones. Do you have any links for me or others following along on that? I figure the old wisdom augmented with lessons learned from LANGSEC stuff will be a good start.
" This is exactly as it should be, since Coq is focused precisely on the domain of functional algorithms (and proofs). And, I have found that, within that domain, the restriction that all my algorithms must provably terminate is nearly invisible."
Wait, are we discussing avoiding Turing completeness or requirements for a termination proof? Termination proofs are done on code in Turing complete languages many times a year in academia. Harder than Coq model of an algorithm for sure but way more useful. I'll just let you elaborate on why you focused on that point.
So, trying to cut through the fog that remains, would you say a good approach is using a language like Haskell or ML that compiles to System F (Turing incomplete) with DSL's where possible? Aside from your DSL point, is building on or alternatives to things like System F what you would like to see?
" Turing-completeness is not a feature I need in a programming language."
Curious, how do you handle I/O and other OS interaction without making it so complex a new programmer must learn Haskell, monads, etc? Is there a simple route to that part of things?
Everywhere I've worked, I have seen the same things reimplemented poorly over and over again in general-purpose languages. Every system I've worked on is roughly a mash-up of database, dataflow graph, state machine, work scheduler, IPC, process coordination, programming in the large, and very low-level algorithmic stuff. Each of these could be factored out into a common simple language, but almost invariably they're just patterns imposed on C/C++/Java/what-have-you code. This greatly hampers understanding and analyzability.
There are rare occasions I see DSLs used to fulfill these roles, and it's to great benefit. Working with a well-designed PostgreSQL database rather than some half-baked home-grown object database is a dream. You get a concurrency model that works, and you can extract graphs of your data model for free. Same with using a state machine description language like SMC rather than hand-coding stuff as C++ boilerplate. Same with using a process coordinator like Erlang's OTP (which isn't a DSL but is close enough).
I'm not writing these posts to try to get developers to use DSLs more often. I'm writing them to try to get language designers to design DSLs more often.
On Coq:
Coq is not at all a practical programming language, since it has no concept of communication with external processes (i.e. I/O). This is exactly as it should be, since Coq is focused precisely on the domain of functional algorithms (and proofs). And, I have found that, within that domain, the restriction that all my algorithms must provably terminate is nearly invisible.
There is a very simple general way to ensure that all programs in Coq terminate: augment each recursive function with one additional argument which is a counter which must always count down to 0 (at which point recursion must halt). On the initial call to a recursive function, select a starting value for this counter which is greater than the number of iterations the algorithm requires. (When proving correctness in Coq, you will be asked to prove that this starting value is in fact suitably high.)
I have kept this requirement in mind when designing programs in other languages, and I have found it trivial to meet in all cases. Turing-completeness is not a feature I need in a programming language.