I don't understand this paragraph. If they do have do-while loops, how do they prevent turing completeness?
ATS has this kind of proof built into the language, so that the type system helps you prove that a loop will always exit, and if it can't, it's a compile error.
It's not entirely clear how useful this is in practice. While you may be able to prove that a loop always exits, it can prove nothing about how long it will take before it does. A loop never terminating, and one that terminates some time after the Milky Way has merged with Andromeda is pretty much equivalent from a practical standpoint.
In particular, if we only care whether something exists then we can accept a long-running computation as proof without having to run it, whilst an infinite loop may be false. For example, a function which takes a list, an index and a proof that the index occurs in the list: we can look up the index safely, without having to care about the actual contents of the proof (the language ensures it's valid).
On the other hand, we can write an infinite loop which claims to prove anything we like, but never actually has to cough up anything. For example:
ProofOfRiemannConjecture myProof {
while (true) {}
}However, we do have a restricted version of `do-while` implemented as described in the Sequential Algorithms RFC[1]. We want to push people into writing parallelizable code by having the default constructs and data types encouraging that, but we know certain algorithms are only possible in a sequential form, and some of them (like the Newton-Raphson method) are not predictable in the number of sequences to run so we have an escape hatch in the language that lets you do the classic iterative programming, but all of them wrapped in a maximum iteration counter so we'll still be able to assign a maximum expected runtime to them (and be sure they halt, perhaps with an error).
[1]: https://github.com/alantech/alan/blob/main/rfcs/007%20-%20Se...
By doing this, loops can be checked before execution to prevent infinite loops and so constrain that as a Turing Machine construct.
I think the underlying good idea here is that Turing Completeness is maybe overrated. You could argue that most good programming languages are good because of what they don't let you do - constraints around how state is mutated is core to Object-oriented and functional programming. Adding some more constraints to ensure complete and reliable static analysis sounds like an excellent idea to me.