Is there any practical programming language (or dialect, or static checker) that enforces this property? Or is Viper the first attempt at a usable, yet decidable language?
I could think of some examples, but you might disagree on the "practical" part.
If I recall correctly, Pascal-style languages have counting for loops where you cannot modify the loop counter or the loop bound inside the loop. That is, you must use a while or repeat loop or recursion to have non-termination. A Pascal compiler would be trivial to extend with syntactic checks for the absence of such loops and recursion. But I don't think it's been done.
You could go towards more programming flexibility but a higher proof burden and use Spark/Ada (for Ada) or Frama-C (for C), but you would need to annotate loops with variant expressions to help the system prove termination.
Note that if you find languages without general loops and without recursion impractical, you might be disappointed by Viper as well. According to the grammar given on GitHub, Viper only has counting loops and no function calls at all except to a few built-in functions. The latter might just be an oversight, though. Functions are too useful to get rid of completely.
If I recall correctly, Pascal-style languages have counting for loops where you cannot modify the loop counter or the loop bound inside the loop. That is, you must use a while or repeat loop or recursion to have non-termination. A Pascal compiler would be trivial to extend with syntactic checks for the absence of such loops and recursion. But I don't think it's been done.
You could go towards more programming flexibility but a higher proof burden and use Spark/Ada (for Ada) or Frama-C (for C), but you would need to annotate loops with variant expressions to help the system prove termination.
Note that if you find languages without general loops and without recursion impractical, you might be disappointed by Viper as well. According to the grammar given on GitHub, Viper only has counting loops and no function calls at all except to a few built-in functions. The latter might just be an oversight, though. Functions are too useful to get rid of completely.