Take the set of all finite C programs without loops or recursive function calls. They (clearly?) halt. Or: the set of all finite Brainfuck programs that don't

Take the set of all finite C programs without loops or recursive function calls. They (clearly?) halt. Or: the set of all finite Brainfuck programs that don't contain a `[` or `]` instruction. Those also halt. Also, see Idris: https://www.idris-lang.org/ https://www.idris-lang.org/. It's a language that has dependent types and a totality checker. A dependent type is a value which depends on another value. For example, the length of an array depends on how many elements there are in the array. A totality checker means that you must prove that a program that you write halts; otherwise, it fails to compile. In Idris, if you ever write the equivalent of reduce recursively, you must prove that the recursion will terminate. This is done by noting that the length of an array is dependent on how many elements are in the array, noting that if an array has zero length then reduce will terminate, and noting that every time reduce is called with a non-zero array length it returns reduce called with that array length decremented by one. Then, since repeatedly subtracting one from a positive number eventually reaches zero (at which point the recursion halts) you're guaranteed that your reduce function halts. EDIT: I guess you are right in the strict sense that languages like Idris aren't Turing complete. But they still can do a huge number of computable and useful things (and most of the things you'd want other languages to do), so I feel like "Turing complete" is mostly a semantic argument here.