Thanks for the writeup. I think this is spot on. I've argued for DSLs many times here on HN due to a slightly different, although intimately related, reason.

Thanks for the writeup. I think this is spot on. I've argued for DSLs many times here on HN due to a slightly different, although intimately related, reason. I think it's the only way to avoid the Turing tarpit [1]. In other words, getting some clean semantics where it is easy to prove things. IMHO, the only way to get formal methods to scale. [1] https://en.wikipedia.org/wiki/Turing_tarpit https://en.wikipedia.org/wiki/Turing_tarpit