So the authors claim that their language is guaranteed to terminate for all well-typed programs. That is actually a nice spot for configuration languages. Yet, I wonder how
a) they guarantee it, as I have seen no obvious link to the language's semantics
Build systems tend to get very complex Turing complete scripts, such as gradle for Java or Make for C. Having something almost as powerful but reducible to a normal form is very helpful for CASE tools.
Banning Turing completeness doesn't give you the property you want, though. Knowing that reducing to a normal form eventually terminates if you wait a million years may be something mathematicians care about, but isn't of practical use.
What matters is that you can analyze the code quickly. To find that out, one way is to try it and kill the process if it takes too long.
Or perhaps better would be to come up with a portable definition of what "takes too long" means that you can put in a presubmit check. Something like "running out of gas" in Ethereum.
So the authors claim that their language is guaranteed to terminate for all well-typed programs. That is actually a nice spot for configuration languages. Yet, I wonder how
a) they guarantee it, as I have seen no obvious link to the language's semantics
b) useful this is in practice.
Nevertheless, very nice approach, indeed.