What practical advantages are there? Someone can always write a program that runs until the heat death of the universe even in a Turing-incomplete language.
The major advantage of a language that isn't Turing complete is not having the major risk inherent to Turing complete languages: asking if any non-trivial program will produce any given result or behavior is undecidable[1].
> write a program that runs until the heat death of the universe even in a Turing-incomplete language.
The Halting Problem is just a simple example of program behavior. The undecidability extends to any other behavior. Asking if a given program will behave maliciously is still undecidable even if we only consider the set of programs that do halt in a reasonable amount of time.
When you are using a regular language or deterministic pushdown automata, questions about the behavior or even asking if two implementations are equivalent is decidable. It is at lest possible8 to create software/tools to help answer the question "is this input safe." When you use a non-deterministic pushdown automata or stronger, you problem becomes provably undecidable*,
I highly recommend the talk "The Science of Insecurity"[2].
> The major advantage of a language that isn't Turing complete is not having the major risk inherent to Turing complete languages: asking if any non-trivial program will produce any given result or behavior is undecidable[1].
It's not obvious to me that I should care about this property in a configuration language. For a given configuration use case, I probably have a good idea about the extreme upper-bound for a correct program--say, 5s. If the program runs for 30s, the supervisor kills it.
> The Halting Problem is just a simple example of program behavior. The undecidability extends to any other behavior. Asking if a given program will behave maliciously is still undecidable even if we only consider the set of programs that do halt in a reasonable amount of time.
What's a malicious action in a configuration use case that a Turing complete program could muster but not a non-Turing-complete program?
In theory that's true for many of the kinds of Turing-incomplete languages we care about. (Eg it's not true for JPG or for (proper) regular expressions.)
From Dhall's docs (emphasis mine):
> Note that a “finite amount of time” can still be very long. For example, there are some short pathological programs that take longer than the heat death of the universe to evaluate. The main benefit of evaluation being finite is not to eliminate long-running programs but to make them significantly less probable. In practice, you will discover that you will rarely author a configuration file that takes a long time to evaluate by accident.
> For example, Dhall does not provide language support for recursion. If you try to define a recursive expression or function you will get a type error. Lists are the only recursive data structure and the only way to build or consume lists is through safe primitives guaranteed to terminate, like List/fold. This restrictive programming style keeps code simple and makes expensive code more obvious (both to the code author and reviewer).
I guess I don’t care much if a configuration language takes a long time in some pathological case (a user writes a loop that doesn’t terminate). Such cases are already too rare to justify a dedicated language. And if the concern is bad actors, then a bad actor wouldn’t have to try to hard to get a Dhall program to run for a long time (copy paste something from the Internet). The more compelling reason to use Dhall is the static type system which is sadly uncommon among configuration languages.
So common that it justifies a change of language? "Oops, this thing that should have run for 5s has run for 30s, something must be wrong, <cancel>". You can even automate that reasoning by way of a timeout. In a hypothetical world where I'm choosing between two otherwise exactly equal configuration languages, I suppose this would give the advantage to Dhall, but honestly I'd probably pick TypeScript because making an entire org learn a new syntax is far more trouble than that saved by non-Turing-completeness.
Totality checking like that in Idris is one nice example. That's kind of circular though - it isn't Turing complete because it has totality checking (i.e. you must prove the program terminates).
