[nextos]

Yes, I think we should build more DSL toolkits. Turing-complete languages are too expressive.

If we had a meta-language like Lisp or ML that had very good capabilities to quickly develop DSLs with very clean restricted semantics for every particular component of a big system, and tooling to automate proofs for said restricted DSLs, software would be more robust and easy to develop.

Alan Kay was pursuing parts of this vision at Viewpoints Research Institute. Racket is also very focused on DSLs. Any others?

[oblio]

90%[1] of popular DSLs turn into Turing-complete languages over time. And they usually end up as very badly designed Turing-complete languages.

[1] Or some other made up, but still very high number.