[towawy]

You can also construct programs in Turing complete languages to always halt (e.g. by bounding the number of iterations of all loops, usually with the tradeoff of limited input size).

[eru]

Yes, you can program in a subset of your language that is not Turing complete.

[The_Colonel]

You'd also need to forbid (even indirect) recursion, i. e. one function cannot appear in a callstack twice.

[trealira]

Isn't that overly restrictive? Some programs are guaranteed to terminate even with mutual recursion.

For example, these (obviously inefficient) functions always terminate for all values of x, since both terminate given an input of 0, and 0 is the minimum possible input to these functions.

  bool even(unsigned int x)
  {
    return (n == 0) ? true : odd(n - 1);
  }

  bool odd(unsigned int x)
  {
    return (n == 0) ? false : even(n - 1);
  }

[eru]

Agda doesn't need that restriction, as far as I know. And neither does Dhall. See https://dhall-lang.org/

Neither language is Turing complete.

[zmgsabst]

I think you can allow finite recursions, eg, a maximum stack depth.