I have been thinking lately that perhaps in the future a lot of software will be built using DSLs, to enable cost-effective formal verification. Turing-complet

I have been thinking lately that perhaps in the future a lot of software will be built using DSLs, to enable cost-effective formal verification. Turing-complete languages have an excessively broad semantics, which makes it hard to prove things about programs written with them. An alternative would be to build tools that allow engineers to develop DSLs quickly, and to then verify properties in programs written using said DSLs. I can see some early signs of this trend in Idris, which is emphasizing DSL-building tools, or in smart contract projects, which are rushing to build contract languages with restricted semantics. There's also related work in Haskell and Racket / Scheme.