> as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the proble

> as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest. Alas, this was proven wrong for verification in 2005. See https://pron.github.io/posts/correctness-and-complexity#correctness-does-not-decompose https://pron.github.io/posts/correctness-and-complexity#corr... > Since your objections applies to a different set of languages than those I'm talking about, your objections are moot. 1. I reject your examples on the ground that they're considered insufficient for their own domains, and in any case are so restricted that you could not compose the lion share of an application from them even without the theorem showing that you cannot reduce the cost of composition by verifying simple components. 2. While I'm happy to further ponder the utility of the languages you listed, you should bear in mind that, say, a Java program using similar constructs to a Sieve program can be reasoned about automatically by current tools, and with relative ease. In other words, a program so simple is easy to reason about whether it's written in a restricted or a non-restricted language, so using those DSLs just increases the cost of verification. However, that does not mean they are not useful. For example, I read that the main design object of Sieve is to allow servers to run untrusted code.