[eru]

Most digital computers are Turing complete, but interestingly not all programming languages are Turing complete.

Turing completeness is a tar pit that makes your code hard to analyse and optimise. It's an interesting challenge to find languages that allow meaningful and useful computation that are not Turing complete. Regular expressions and SQL-style relational algebra (but not Perl-style regular expressions nor most real-world SQL dialects) are examples familiar to many programmers.

Programming languages like Agda and Idris that require that you prove that your programs terminate [0] are another interesting example, less familiar to people.

[0] It's slightly more sophisticated than this: you can also write event-loops that go on forever, but you have to prove that your program does some new IO after a finite amount of time. (Everything oversimplified here.)

[kragen]

yes, total functional programming is an interesting research area, and of course almost all of our subroutines are intended to verifiably terminate

[eru]

I'm not even sure total programming needs to be functional. That's just the most common way to do it, I guess, because functional programming is a good vehicle for 'weird' theoretical computer science ideas.