<p>I'm trying to teach a friend to code in Python. I've noticed that whenever they write a while loop with an integer increment, such as the one shown below:</p>
<pre class="lang-python prettyprint-override"><code>i = 0
while i &lt; 10:
    do this
    i += 1
</code></pre>
<p>...they always seem to leave out the <code>i += 1</code> at the end, which causes an infinite loop.</p>
<p>How can a linter or something similar check for this error and notify the user?</p>

<syntax><while-loop>
How can the language or tooling notify the user of infinite loops?
<h3>Transforming into Pure, Tail-Recursive Functions Could Help</h3>
<p>Or equivalently, static single assignments and blocks, but tail-recursion is nicer for humans to write.</p>
<p>The advantage here is that it greatly simplifies the analysis. The only way the state can change is to make a tail-call and change all of it at once. The only quantities that can change are the parameters of the function, which are normally listed for you. (This begins to get complicated when you do things like update an array, or make mutually-recursive tail calls, but it’ll do for this special case.</p>
<p>It will be much more convenient to write our loops if we allow certain provably-safe extensions to the subset we can analyze, such as tail-recursion modulo cons.</p>
<p>Another important reason to work on this representation is, most major compilers transform the source code into an intermediate representation in either CPS or SSA form, so an analyzer might be able to work on the IR.</p>
<h3>Annotating to Prove Termination</h3>
<p>A simple example of some hypothetical syntax:</p>
<pre class="lang-haskell prettyprint-override"><code>{- terminating{i &gt; 0} -}
factorial::(Unsigned -&gt; Unsigned)
factorial 0 = 1
factorial i = i * factorial (i-1)
</code></pre>
<p>If we’d written this as a <code>while</code> loop in an imperative language, <code>i&gt;0</code> would have been the loop condition, so this syntax should be intuitive.</p>
<p>Side note: in actually-existing functional languages, you’re more likely to see this expressed as:</p>
<pre class="lang-haskell prettyprint-override"><code>factorial::(Unsigned -&gt; Unsigned)
factorial n = go 1 n where
    {- terminating{i &gt; 0} -}
    go accumulator 0 = accumulator
    go accumulator i = go (accumulator*i) (i-1)
</code></pre>
<p><a href="https://cs.stackexchange.com/questions/83360/what-property-of-cons-allows-elimination-of-tail-recursion-modulo-cons/86036#86036">But in fact the same optimization that allows tail-recursion modulo cons applies to any semigroup operation on a variable.</a>  So I’m just going to assume that our language is smart enough to compile the tail-recursion-modulo-semigroup version efficiently, even though I don’t think compilers in 2023 actually now do this <em>in general</em> and not just for a few special cases. (I would <em>love</em> to find out that I’m wrong.)</p>
<p>In this context, the annotation tells an analyzer what to check: that every branch of the function <strong>either</strong> terminates the loop, <strong>or</strong> calls the function with the new value of <code>i</code> <strong>both</strong> greater than or equal to zero, <strong>and</strong> decreasing.  If these conditions are satisfied, the loop provably terminates.  But if the reason the programmer gave us for believing that the loop terminates was that <code>i</code> decreases to 0, and we can’t convince ourselves that it does, that’s concerning.</p>
<h3>Extending the Syntax</h3>
<p>For symmetry, there should of course be a <code>&lt;</code> condition:</p>
<pre class="lang-haskell prettyprint-override"><code>sum container  = go 0 where
    n = length container
    {- terminating{i &lt; n} -}
    go i | i == n    = 0
         | otherwise = container!i + sum (i+1)
</code></pre>
<p>{This punts on one of the tricky little problems, proving that <code>length container</code> is finite, but since I moved that outside the loop, it’s no longer the loop-analyzer’s problem.)</p>
<p>But what if we want an extension of the factorial over all the integers?</p>
<pre class="lang-haskell prettyprint-override"><code>{- terminating{|i| &gt; 0} -}
factorialEx::(Integer-&gt;Integer)
factorialEx 0             = 1
factorialEx i | i &lt; 0     = -1 * factorialEx(-i - 1)
              | otherwise = i * factorialEx(i - 1)
</code></pre>
<h3>A Canonical Form</h3>
<p>Counting down the absolute value of some quantity toward zero is such a common terminating condition, I’ll delare it the default in this syntax:</p>
<pre class="lang-haskell prettyprint-override"><code>{- terminating{i} -}
</code></pre>
<p>We can easily see that the other two examples so far could also be expressed this way.  Clearly, <code>FactorialEz</code> also has the terminating condition <code>{i}</code>.</p>
<p>We can turn a comparison into a difference very easily:</p>
<pre class="lang-haskell prettyprint-override"><code>sum container  = go 0 where
    n = length container
    {- terminating{n - i} -}
    go i | i == length container = 0
         | otherwise             = container!i + sum (i+1)
</code></pre>
<h3>Expressions as Terminating Conditions</h3>
<p>Sometimes, the well-founded termination condition doesn’t explicitly appear in the code at all, though.  Take for example this merge of ordered lists:</p>
<pre class="lang-haskell prettyprint-override"><code>{- terminating{length first + length second} -}
merge first@[]     second@[]                 = []
merge first        second@[]                 = first
merge first@[]     second                    = second
merge first@(x:xs) second@(y:ys) | y &lt; x     = y:(merge first ys)
                                 | otherwise = x:(merge xs second)
</code></pre>
<p>We can only verify this for all branches if we know that the length of a non-empty list is always larger than the length of its tail, so let’s extend this syntax in an ad-hoc way to be able to tell the compiler that:</p>
<pre class="lang-haskell prettyprint-override"><code>{- terminating{ length [] = 0, length (x:xs) = length xs + 1 ;
                length first + length second } -}
</code></pre>
<p>In practice, such a commonly-used fact should be defined in the standard library, so the compiler remembers it without being told.</p>
<h3>Algorithmically Guessing the Condition</h3>
<p>Will this work for everything?  No, of course not.  Since you’re still reading this far, you’ve seen Alan Turing’s proof that nothing can.  But, in practice, a lot of loops are simple enough to check with a couple of heuristics.</p>
<p>There are usually a small number of variables, two or three, that appear in a terminating condition, and a slightly-larger number of local variables with the right type to make up an arithmetic expression that evaluates to a condition in canonical form, which we know must include at least one of the parameters that gets changed in every call on every branch—if any branch calls the same pure function with the same arguments, that would be an infinite loop.  There are only eight possible arrangements of a, b, and c of the form (a + b + c), (a + b - c), (a - b + c), etc.  There are only three of the form a * (b + c) and another three of the form a + bc.  There are only six of the form a * (b - c) and six of the form a + (b/c).  Check these first.</p>
<p>As this number gets higher, we of course get a combinatorial explosion.  But a human code reviewer would tell a programmer not to write loops with a huge amount of internal state to keep track of, too.  and restricting ourselves to functional programming makes it much easier to see what the possible variables are.</p>
<h3>Future Directions</h3>
<p>A few of the most useful ways this might be extended:</p>
<ul>
<li>Inferring a loop condition that relies on a combination of facts, rather than a single, explicitly-spelled-out fact.</li>
<li><a href="https://en.wikipedia.org/wiki/Mutual_recursion" rel="nofollow noreferrer">Mutual recursion,</a> with conditions that need to span two different functions.</li>
<li>Constraints on the data</li>
<li>An annotation meaning, “This branch doesn’t bring the loop closer to termination, but as you can verify, the recursive call it makes will take a branch that does.”</li>
<li>Disjunctions in the list of givens. For example, either x &lt; y, or x &lt; y, or x == y.</li>
<li>Implications. For example, if x &gt; y, y &lt; x.</li>
</ul>
<h3>Update: Arbitrary State Variables as Conditions</h3>
<p>One idea that came to me last night and I’d like to know if someone has implemented is that many modern languages support sum types (such as Haskell <code>data</code> or Rust <code>enum</code>), and allow the user to define an ordering, partial or total, over them.  If this actually is a true partial ordering, this would allow the compiler to prove the correctness of a loop as general as</p>
<pre class="lang-haskell prettyprint-override"><code>{- terminating{terminalState} -}
loop terminalState = extractResult state
loop state         = loop (update state)
</code></pre>
<p>where this checks that, on every branch that makes a tail-recursive call that updates <code>state</code> to <code>state'</code>, either <code>state</code> &lt; <code>state'</code> ≤ <code>terminalState' or </code>state<code>&gt;</code>state'<code>≥</code>terminalState`.</p>
<p>This wouldn’t work on loops with more than one possible terminal state that a loop might bounce between.  In that case, you’d also need to show that the next branch also moves the state even closer to the <strong>same</strong> terminal state.</p>
<p>A programmer who had this might even write an ordering function that won’t generate executable code, just so the compiler can see it and automatically deduce that the loop terminates.  (It would probably help convince a human that the loop terminates, too.)</p>
<h3>So, Whose Wheel Did I Just Re-Invent?</h3>
<p>I’d be surprised if someone hasn’t worked this out already in much more detail, and published it.  I’d appreciate the citations!</p>

CC BY-SA 4.0
2023-07-23T04:42:12.830Z
2023-07-31T20:18:38.257Z
2023-07-31T20:18:38.257Z
Davislor
CC BY-SA 4.0
2023-07-24T10:40:21.857Z
I believe this is similar to imperative languages that prove loop termination. However, your idea to mark a countdown as a function argument is interesting because it changes the proof requirement. Now you have to prove that in any recursive call, the recursive parameter `i` is smaller than the current parameter `i` and greater than zero, and this is a trivial proof in many cases (e.g. in `factorialEx`). However, having to specify that `i` counts down is still uselessly obscure to the beginner.
Criticize SE actions means ban
CC BY-SA 4.0
2023-07-24T14:09:47.993Z
@user253751 Thanks. The basic idea is that it might be trivial enough for an algorithm to deduce it on its own. And in the cases where it can’t, and asks the programmer to write a proof, the proof language can be as close to the HLL as possible: the proof is, writing out the function that counts down.
Davislor
<p>It is often possible to determine that a loop terminates, or doesn't terminate, through static analysis. While it isn't <em>always</em> possible to determine whether a loop terminates or not, it's a category error to think that this means it's <em>never</em> possible — in fact, <strong>it is frequently possible to detect non-terminating loops automatically</strong>.</p>
<p>Verifying languages like <a href="https://en.wikipedia.org/wiki/Whiley_(programming_language)" rel="noreferrer">Whiley</a> and <a href="https://dafny.org/" rel="noreferrer">Dafny</a> can enforce that loops terminate by checking loop invariants, preconditions, and termination conditions with theorem provers. Sometimes the programmer needs to provide additional annotations to assist the prover when it rejects a program because it couldn't be certain of termination.</p>
<p>In the case of a simple Dafny loop</p>
<pre class="lang-none prettyprint-override"><code>var i := 0;
while i &lt; n
{
  // ... do something ...
}
</code></pre>
<p>the compiler will correctly reject this program as non-terminating, while if <code>i := i + 1</code> were inside the body then the termination checker <em>would</em> verify the program. It <a href="https://dafny.org/dafny/OnlineTutorial/Termination" rel="noreferrer">infers</a> a loop variant <code>decreases n - i</code> from the loop's test condition, and it can easily see that this expression <em>will not</em> decrease because neither <code>i</code> nor <code>n</code> changes within the loop. The termination checker will often just work without further effort from the programmer, even for moderately complex loops.</p>
<p>In still-more-complex loops, the programmer will need to specify loop invariants, pre- and post-conditions, or manual decreases conditions. The verifier will ensure that the program is consistent with these annotations, and that they guarantee the necessary properties. Otherwise, the compiler will reject the program and report to the user with a diagnostic message saying why.</p>

CC BY-SA 4.0
2023-07-22T06:41:04.947Z
2023-07-22T06:41:04.947Z
Michael Homer
CC BY-SA 4.0
2023-07-24T10:35:59.933Z
My feeling is that this is much more confusing for a beginner than simply allowing them to run the program and see it loop forever. In particular, if they have to annotate their loops to prove they terminate, or if the error is anything more complex than "loop never ends", they'll never get into the language at all. I think that a beginner has to make a mistake like this, see the immediate consequences, and then eventually they will appreciate having tools to avoid the mistake, *but only after the mistake frustrates them*.
Criticize SE actions means ban
<h2>Having &quot;for each&quot; loops instead of, or in addition to, &quot;while&quot; loops</h2>
<p>In Python you'd typically loop like:</p>
<pre class="lang-py prettyprint-override"><code>for i in range(10):
    do this
</code></pre>
<p>You don't need to remember to increment <code>i</code>, since the iterator will run over all values.</p>
<p>This also makes it easy to loop over arrays or or other data structures since you don't need to know the length.</p>
<p>Disadvantage is you can't change the value of <code>i</code> inside the loop depending on conditions, at least not without writing your own generator.</p>
<h2>Having a built-in &quot;update slot&quot; in your loop so you know if something is missing</h2>
<p>In C-style languages, you have the 3 part <code>for</code> loop like this:</p>
<pre class="lang-c prettyprint-override"><code>for(int i=0; i&lt;10; i++) {

}
</code></pre>
<p>While you can of course omit the <code>i++</code> if you want:</p>
<pre><code>for (int i=0; i&lt;10;) {}
</code></pre>
<p>However, the slot is still there, will look weird and empty, and act as a sort of &quot;are you sure&quot; spot. If you do want to skip the increment you are making it more explicit.</p>
<h2>Deciding whether a loop will terminate in a linter is undecidable</h2>
<p>That's basically the halting problem. I'd focus instead on designing the language to encourage less error-prone types of loops when possible.</p>
<p>Other methods mentioned in other answers do work, but they require a highly restricted language to be able to effectively rule out side effects and overloads effecting the loop condition.</p>
<p>Even if you do manage to eliminate all possible factors that could cause termination, you still don't know if the loop being infinite is intentional or a mistake. I call this &quot;the meta halting problem&quot;: &quot;Given a oracle for the halting problem, it is still undecidable if the developer intended for this Turing machine to halt.&quot;</p>

CC BY-SA 4.0
2023-07-22T05:55:48.877Z
2023-07-25T07:33:08.730Z
2023-07-25T07:33:08.730Z
mousetail 'he-him'
CC BY-SA 4.0
2023-07-22T18:32:26.940Z
I recently had to write code with one of the three "slots" in a C-style for loop was empty. Yes, it looks weird, _and that's the point._
Bbrk24
CC BY-SA 4.0
2023-07-24T13:54:52.710Z
Minor correction: as pointed out by Michael Homer's answer, a better way to put it is "Deciding whether _every_ loop will terminate in a linter is undecidable". The majority of loops can be relatively easily determined whether they terminate or not, it's just that there always exists at least one way to code a loop where it can't be determined.
Idran
CC BY-SA 4.0
2023-07-24T14:01:49.543Z
@JustinHilyard True, in a way, but the methods mentioned in the other answers are really error prone to implement right, and you can easily create a situation causing unnecessary errors or warnings.
mousetail 'he-him'
CC BY-SA 4.0
2023-07-25T07:06:28.513Z
+1 for using better tools first. `for` loops should be the goto. `while` loops should only be used when the condition/iteration is tricky. Not only does this guideline means you'll avoid iteration issues most of the time (by using `for`), it also means that any `while` loop should get extra scrutiny with regard to its iteration, and therefore any mistake _there_ is more likely to be caught.
Matthieu M.
CC BY-SA 4.0
2023-08-07T14:53:03.887Z
One thing to note about for-each loops is that if iterators can be user-defined ─ which they can in most languages that have for-each loops ─ then it's no longer guaranteed that for-each loops terminate, because the user can define an infinite iterator. As an aside, "the goto" is a funny way of describing which control-flow statement should be preferred :D
kaya3
<p>Some languages allow only loops that can be <strong>proved</strong> to terminate.</p>
<p>One example of this is eBPF, which includes a <a href="https://ebpf.io/what-is-ebpf/#verifier" rel="noreferrer">bytecode verification</a> step before a program is allowed to run:</p>
<blockquote>
<p>... the program is only accepted if the verifier can ensure that the loop contains an exit condition which is guaranteed to become true.</p>
</blockquote>
<p>The verifier avoids the Halting Problem by rejecting programs that are too complex for verification within a reasonable budget:</p>
<blockquote>
<p>Program must have a finite complexity. The verifier will evaluate all possible execution paths and must be capable of completing the analysis within the limits of the configured upper complexity limit.</p>
</blockquote>

CC BY-SA 4.0
2023-07-22T08:37:17.520Z
2023-07-22T08:37:17.520Z
Toby Speight
CC BY-SA 4.0
2023-07-22T10:51:59.923Z
Another such example - total functional programming, where recursion is always guaranteed to terminate.
SK-logic
CC BY-SA 4.0
2023-07-25T15:30:32.310Z
A loop that is proved to terminate after 2^64 is practically infinite.
gnasher729
<p>While it is not possible to solve this problem in general (see the <a href="https://en.wikipedia.org/wiki/Halting_problem" rel="noreferrer">halting problem</a>) it is certainly possible to solve it in some very common cases.</p>
<p>For example, in C# if you enter this:</p>
<pre><code>var i = 0;
while (i &lt; 10) {
    Console.WriteLine(i);
}
</code></pre>
<p>The editor will put a wiggly line under the while condition and warn that &quot;this condition is always true.&quot; FWIW, I'd prefer it considered it an actual error, but that is beside the point. In the specific case you mention it is certainly solvable.</p>
<p>The data flow analysis of the compiler can determine which variables can be changed and in what part of the code. Here is is relatively simple since the variable is local, and so has visibility only in the block, and the parameter passed to Console.Writeline is pass by value. It is certainly possible to do it at a larger scale by tracing what functions can change what variables. For example if this was a property of a class, if private you can readily determine which methods in the class can change that property, since they are the only ones that have access to it.</p>
<p>In languages like C++ this ability is enhanced by the use of const correctness, where the programmer can explicitly specify to the compiler (and the compiler can enforce) these types of rules, enhancing the ability of the dfa to detect this sort of thing.</p>
<p>So it can be done, and it often is done, for many of the most common cases. It can't be done for all cases, and it is harder in lower level languages like C++ where references to variables and aliases can rather easily be hidden, especially if the programmer isn't careful about their const correctness. In these cases the compiler will still produce correct code, just that it'll be more conservative, and more of the &quot;common cases&quot; I mentioned will be considered indeterminable.</p>
<p>I'm not a Python guy, but for sure Python COULD do this too. If it doesn't I'd consider that a shortcoming in the compiler or interpreter you are using.</p>

CC BY-SA 4.0
2023-07-23T19:19:10.907Z
2023-07-23T19:19:10.907Z
Fraser Orr
CC BY-SA 4.0
2023-07-24T10:41:48.600Z
I would not recommend making this an actual error because there is more stuff to understand before you can understand the error. The beginner may not understand why the error is there, without reading a bunch of theory - until he actually runs the program and it loops forever, and then he will *instantly* understand it. The epiphany can't happen if you stop him from running the program.
Criticize SE actions means ban
CC BY-SA 4.0
2023-07-24T16:55:37.850Z
Aside from that, it's useful to be able to write programs that don't offer an explicit exit.
Karl Knechtel
CC BY-SA 4.0
2023-07-25T04:40:37.627Z
@KarlKnechtel that's an excellent point. There is the classic for(;;) C idiom. But for sure I'd upgrade it to a warning at least.
Fraser Orr
<p>Simplest check that some languages are already doing is to see if any variables involved in the loop condition check are modified, or otherwise if any break or return statement exists in the loop.</p>
<p>While this is not always (reading from the default input stream would change the loop condition without modifying any visible variables), this would catch majority of errors.</p>

CC BY-SA 4.0
2023-08-04T07:31:18.300Z
2023-08-04T07:31:18.300Z
Audrius Meškauskas
<h2>Low-hanging fruit</h2>
<p>Of course, the halting problem is undecidable. However, linters don't have to be perfectly logical, because they emit warnings that aren't even from the code itself (i.e. they can be completely bypassed by not using the IDE).</p>
<p>A huge fraction of errors of this sort will involve the situation where <em>none of the identifiers in the <code>while</code> expression are used at all in the loop body</em>, and there is also no explicit <code>break</code>, <code>return</code> or other deliberate exit. Technically, such a loop could still terminate (say, if the expression involves a call to a function that has side effects, or an exception is raised), but in the vast majority of cases, code shaped like this will be problematic. So a rule like this is Good Enough for a linter.</p>

CC BY-SA 4.0
2023-07-22T06:15:18.107Z
2023-07-22T18:18:08.937Z
2023-07-22T18:18:08.937Z
Karl Knechtel
CC BY-SA 4.0
2023-07-22T14:00:41.167Z
Don't forget the `break` statements (if your language has them).
Vilx-
CC BY-SA 4.0
2023-07-22T14:10:46.863Z
Linters do have to be perfectly logical, because they are deterministic algorithms running on deterministic computers. Whether they ever produce false negatives is another matter.
user3840170
CC BY-SA 4.0
2023-07-22T14:41:44.740Z
Yes, that's the important thing: *undecidable*. However it could probably be done rigorously if the behaviour were detectable at compilation time, i.e. no functions with side-effects invoked etc., no parallel processing, no interrupt handlers... ... all in all, it might be better simply to teach the student that it's something to watch out for.
Mark Morgan Lloyd
CC BY-SA 4.0
2023-07-22T18:18:17.470Z
@Vilx- edited accordingly.
Karl Knechtel
CC BY-SA 4.0
2023-07-22T18:19:03.623Z
@user3840170 I don't mean "could perform illogically"; I mean "are not required to implement logic that perfectly addresses the problem".
Karl Knechtel
CC BY-SA 4.0
2023-07-24T16:52:41.320Z
@MarkMorganLloyd I agree; but I don't think linters make good tutors in the first place.
Karl Knechtel
CC BY-SA 4.0
2023-07-24T18:00:31.597Z
@KarlKnechtel well, it wasn't me who introduced linters. However I think that they actually cover two separate areas: (a) things that a compiler can and arguably should check for e.g. an infinite loop which has no chance whatsoever of exiting (b) heuristics which very often indicate a /possible/ problem.
Mark Morgan Lloyd
CC BY-SA 4.0
2023-08-04T16:43:49.947Z
From a language design perspective, having compiler generated code throw an exception or raise a panic in cases where an implementation happens to recognizes that execution has reached point from which there are no reachable side effects downstream could be useful, if code needing the loop-endlessly behavior could install a handler for that purpose.
supercat
# How can the language or tooling notify the user of infinite loops?
Posted by: username_0 on 2023-07-22
I'm trying to teach a friend to code in Python. I've noticed that whenever they write a while loop with an integer increment, such as the one shown below:
i = 0
while i < 10:
    do this
    i += 1

...they always seem to leave out the i += 1 at the end, which causes an infinite loop.
How can a linter or something similar check for this error and notify the user?
**Tags:** syntax while-loop
---
## 7 answers
### Answer by username_13 on 2023-07-22. Score: 39 | Accepted answer
## Low-hanging fruit

Of course, the halting problem is undecidable. However, linters don't have to be perfectly logical, because they emit warnings that aren't even from the code itself (i.e. they can be completely bypassed by not using the IDE).

A huge fraction of errors of this sort will involve the situation where *none of the identifiers in the `while` expression are used at all in the loop body*, and there is also no explicit `break`, `return` or other deliberate exit. Technically, such a loop could still terminate (say, if the expression involves a call to a function that has side effects, or an exception is raised), but in the vast majority of cases, code shaped like this will be problematic. So a rule like this is Good Enough for a linter.
> **Comments:**
> **username_15** (2023-07-22): Don't forget the `break` statements (if your language has them).  
> **username_16** (2023-07-22): Linters do have to be perfectly logical, because they are deterministic algorithms running on deterministic computers. Whether they ever produce false negatives is another matter.  
> **username_17** (2023-07-22): Yes, that's the important thing: *undecidable*. However it could probably be done rigorously if the behaviour were detectable at compilation time, i.e. no functions with side-effects invoked etc., no parallel processing, no interrupt handlers... ... all in all, it might be better simply to teach the student that it's something to watch out for.  
> **username_13** (2023-07-22): @Vilx- edited accordingly.  
> **username_13** (2023-07-22): @user3840170 I don't mean "could perform illogically"; I mean "are not required to implement logic that perfectly addresses the problem".  
> **username_13** (2023-07-24): @MarkMorganLloyd I agree; but I don't think linters make good tutors in the first place.  
> **username_17** (2023-07-24): @KarlKnechtel well, it wasn't me who introduced linters. However I think that they actually cover two separate areas: (a) things that a compiler can and arguably should check for e.g. an infinite loop which has no chance whatsoever of exiting (b) heuristics which very often indicate a /possible/ problem.  
> **username_18** (2023-08-04): From a language design perspective, having compiler generated code throw an exception or raise a panic in cases where an implementation happens to recognizes that execution has reached point from which there are no reachable side effects downstream could be useful, if code needing the loop-endlessly behavior could install a handler for that purpose.  
---
### Answer by username_3 on 2023-07-22. Score: 27
It is often possible to determine that a loop terminates, or doesn't terminate, through static analysis. While it isn't always possible to determine whether a loop terminates or not, it's a category error to think that this means it's never possible — in fact, it is frequently possible to detect non-terminating loops automatically.
Verifying languages like Whiley and Dafny can enforce that loops terminate by checking loop invariants, preconditions, and termination conditions with theorem provers. Sometimes the programmer needs to provide additional annotations to assist the prover when it rejects a program because it couldn't be certain of termination.
In the case of a simple Dafny loop
var i := 0;
while i < n
{
  // ... do something ...
}

the compiler will correctly reject this program as non-terminating, while if i := i + 1 were inside the body then the termination checker would verify the program. It infers a loop variant decreases n - i from the loop's test condition, and it can easily see that this expression will not decrease because neither i nor n changes within the loop. The termination checker will often just work without further effort from the programmer, even for moderately complex loops.
In still-more-complex loops, the programmer will need to specify loop invariants, pre- and post-conditions, or manual decreases conditions. The verifier will ensure that the program is consistent with these annotations, and that they guarantee the necessary properties. Otherwise, the compiler will reject the program and report to the user with a diagnostic message saying why.
> **Comments:**
> **username_2** (2023-07-24): My feeling is that this is much more confusing for a beginner than simply allowing them to run the program and see it loop forever. In particular, if they have to annotate their loops to prove they terminate, or if the error is anything more complex than "loop never ends", they'll never get into the language at all. I think that a beginner has to make a mistake like this, see the immediate consequences, and then eventually they will appreciate having tools to avoid the mistake, *but only after the mistake frustrates them*.  
---
### Answer by username_4 on 2023-07-22. Score: 20
Having "for each" loops instead of, or in addition to, "while" loops
In Python you'd typically loop like:
for i in range(10):
    do this

You don't need to remember to increment i, since the iterator will run over all values.
This also makes it easy to loop over arrays or or other data structures since you don't need to know the length.
Disadvantage is you can't change the value of i inside the loop depending on conditions, at least not without writing your own generator.
Having a built-in "update slot" in your loop so you know if something is missing
In C-style languages, you have the 3 part for loop like this:
for(int i=0; i<10; i++) {

}

While you can of course omit the i++ if you want:
for (int i=0; i<10;) {}

However, the slot is still there, will look weird and empty, and act as a sort of "are you sure" spot. If you do want to skip the increment you are making it more explicit.
Deciding whether a loop will terminate in a linter is undecidable
That's basically the halting problem. I'd focus instead on designing the language to encourage less error-prone types of loops when possible.
Other methods mentioned in other answers do work, but they require a highly restricted language to be able to effectively rule out side effects and overloads effecting the loop condition.
Even if you do manage to eliminate all possible factors that could cause termination, you still don't know if the loop being infinite is intentional or a mistake. I call this "the meta halting problem": "Given a oracle for the halting problem, it is still undecidable if the developer intended for this Turing machine to halt."
> **Comments:**
> **username_5** (2023-07-22): I recently had to write code with one of the three "slots" in a C-style for loop was empty. Yes, it looks weird, _and that's the point._  
> **username_6** (2023-07-24): Minor correction: as pointed out by Michael Homer's answer, a better way to put it is "Deciding whether _every_ loop will terminate in a linter is undecidable". The majority of loops can be relatively easily determined whether they terminate or not, it's just that there always exists at least one way to code a loop where it can't be determined.  
> **username_4** (2023-07-24): @JustinHilyard True, in a way, but the methods mentioned in the other answers are really error prone to implement right, and you can easily create a situation causing unnecessary errors or warnings.  
> **username_7** (2023-07-25): +1 for using better tools first. `for` loops should be the goto. `while` loops should only be used when the condition/iteration is tricky. Not only does this guideline means you'll avoid iteration issues most of the time (by using `for`), it also means that any `while` loop should get extra scrutiny with regard to its iteration, and therefore any mistake _there_ is more likely to be caught.  
> **username_8** (2023-08-07): One thing to note about for-each loops is that if iterators can be user-defined ─ which they can in most languages that have for-each loops ─ then it's no longer guaranteed that for-each loops terminate, because the user can define an infinite iterator. As an aside, "the goto" is a funny way of describing which control-flow statement should be preferred :D  
---
### Answer by username_9 on 2023-07-22. Score: 15
Some languages allow only loops that can be **proved** to terminate.

One example of this is eBPF, which includes a [bytecode verification](https://ebpf.io/what-is-ebpf/#verifier) step before a program is allowed to run:

> ... the program is only accepted if the verifier can ensure that the loop contains an exit condition which is guaranteed to become true.

The verifier avoids the Halting Problem by rejecting programs that are too complex for verification within a reasonable budget:

> Program must have a finite complexity. The verifier will evaluate all possible execution paths and must be capable of completing the analysis within the limits of the configured upper complexity limit.
> **Comments:**
> **username_10** (2023-07-22): Another such example - total functional programming, where recursion is always guaranteed to terminate.  
> **username_11** (2023-07-25): A loop that is proved to terminate after 2^64 is practically infinite.  
---
### Answer by username_1 on 2023-07-23. Score: 9
Transforming into Pure, Tail-Recursive Functions Could Help
Or equivalently, static single assignments and blocks, but tail-recursion is nicer for humans to write.
The advantage here is that it greatly simplifies the analysis. The only way the state can change is to make a tail-call and change all of it at once. The only quantities that can change are the parameters of the function, which are normally listed for you. (This begins to get complicated when you do things like update an array, or make mutually-recursive tail calls, but it’ll do for this special case.
It will be much more convenient to write our loops if we allow certain provably-safe extensions to the subset we can analyze, such as tail-recursion modulo cons.
Another important reason to work on this representation is, most major compilers transform the source code into an intermediate representation in either CPS or SSA form, so an analyzer might be able to work on the IR.
Annotating to Prove Termination
A simple example of some hypothetical syntax:
{- terminating{i > 0} -}
factorial::(Unsigned -> Unsigned)
factorial 0 = 1
factorial i = i * factorial (i-1)

If we’d written this as a while loop in an imperative language, i>0 would have been the loop condition, so this syntax should be intuitive.
Side note: in actually-existing functional languages, you’re more likely to see this expressed as:
factorial::(Unsigned -> Unsigned)
factorial n = go 1 n where
    {- terminating{i > 0} -}
    go accumulator 0 = accumulator
    go accumulator i = go (accumulator*i) (i-1)

But in fact the same optimization that allows tail-recursion modulo cons applies to any semigroup operation on a variable.  So I’m just going to assume that our language is smart enough to compile the tail-recursion-modulo-semigroup version efficiently, even though I don’t think compilers in 2023 actually now do this in general and not just for a few special cases. (I would love to find out that I’m wrong.)
In this context, the annotation tells an analyzer what to check: that every branch of the function either terminates the loop, or calls the function with the new value of i both greater than or equal to zero, and decreasing.  If these conditions are satisfied, the loop provably terminates.  But if the reason the programmer gave us for believing that the loop terminates was that i decreases to 0, and we can’t convince ourselves that it does, that’s concerning.
Extending the Syntax
For symmetry, there should of course be a < condition:
sum container  = go 0 where
    n = length container
    {- terminating{i < n} -}
    go i | i == n    = 0
         | otherwise = container!i + sum (i+1)

{This punts on one of the tricky little problems, proving that length container is finite, but since I moved that outside the loop, it’s no longer the loop-analyzer’s problem.)
But what if we want an extension of the factorial over all the integers?
{- terminating{|i| > 0} -}
factorialEx::(Integer->Integer)
factorialEx 0             = 1
factorialEx i | i < 0     = -1 * factorialEx(-i - 1)
              | otherwise = i * factorialEx(i - 1)

A Canonical Form
Counting down the absolute value of some quantity toward zero is such a common terminating condition, I’ll delare it the default in this syntax:
{- terminating{i} -}

We can easily see that the other two examples so far could also be expressed this way.  Clearly, FactorialEz also has the terminating condition {i}.
We can turn a comparison into a difference very easily:
sum container  = go 0 where
    n = length container
    {- terminating{n - i} -}
    go i | i == length container = 0
         | otherwise             = container!i + sum (i+1)

Expressions as Terminating Conditions
Sometimes, the well-founded termination condition doesn’t explicitly appear in the code at all, though.  Take for example this merge of ordered lists:
{- terminating{length first + length second} -}
merge first@[]     second@[]                 = []
merge first        second@[]                 = first
merge first@[]     second                    = second
merge first@(x:xs) second@(y:ys) | y < x     = y:(merge first ys)
                                 | otherwise = x:(merge xs second)

We can only verify this for all branches if we know that the length of a non-empty list is always larger than the length of its tail, so let’s extend this syntax in an ad-hoc way to be able to tell the compiler that:
{- terminating{ length [] = 0, length (x:xs) = length xs + 1 ;
                length first + length second } -}

In practice, such a commonly-used fact should be defined in the standard library, so the compiler remembers it without being told.
Algorithmically Guessing the Condition
Will this work for everything?  No, of course not.  Since you’re still reading this far, you’ve seen Alan Turing’s proof that nothing can.  But, in practice, a lot of loops are simple enough to check with a couple of heuristics.
There are usually a small number of variables, two or three, that appear in a terminating condition, and a slightly-larger number of local variables with the right type to make up an arithmetic expression that evaluates to a condition in canonical form, which we know must include at least one of the parameters that gets changed in every call on every branch—if any branch calls the same pure function with the same arguments, that would be an infinite loop.  There are only eight possible arrangements of a, b, and c of the form (a + b + c), (a + b - c), (a - b + c), etc.  There are only three of the form a * (b + c) and another three of the form a + bc.  There are only six of the form a * (b - c) and six of the form a + (b/c).  Check these first.
As this number gets higher, we of course get a combinatorial explosion.  But a human code reviewer would tell a programmer not to write loops with a huge amount of internal state to keep track of, too.  and restricting ourselves to functional programming makes it much easier to see what the possible variables are.
Future Directions
A few of the most useful ways this might be extended:

Inferring a loop condition that relies on a combination of facts, rather than a single, explicitly-spelled-out fact.
Mutual recursion, with conditions that need to span two different functions.
Constraints on the data
An annotation meaning, “This branch doesn’t bring the loop closer to termination, but as you can verify, the recursive call it makes will take a branch that does.”
Disjunctions in the list of givens. For example, either x < y, or x < y, or x == y.
Implications. For example, if x > y, y < x.

Update: Arbitrary State Variables as Conditions
One idea that came to me last night and I’d like to know if someone has implemented is that many modern languages support sum types (such as Haskell data or Rust enum), and allow the user to define an ordering, partial or total, over them.  If this actually is a true partial ordering, this would allow the compiler to prove the correctness of a loop as general as
{- terminating{terminalState} -}
loop terminalState = extractResult state
loop state         = loop (update state)

where this checks that, on every branch that makes a tail-recursive call that updates state to state', either state < state' ≤ terminalState' or state>state'≥terminalState`.
This wouldn’t work on loops with more than one possible terminal state that a loop might bounce between.  In that case, you’d also need to show that the next branch also moves the state even closer to the same terminal state.
A programmer who had this might even write an ordering function that won’t generate executable code, just so the compiler can see it and automatically deduce that the loop terminates.  (It would probably help convince a human that the loop terminates, too.)
So, Whose Wheel Did I Just Re-Invent?
I’d be surprised if someone hasn’t worked this out already in much more detail, and published it.  I’d appreciate the citations!
> **Comments:**
> **username_2** (2023-07-24): I believe this is similar to imperative languages that prove loop termination. However, your idea to mark a countdown as a function argument is interesting because it changes the proof requirement. Now you have to prove that in any recursive call, the recursive parameter `i` is smaller than the current parameter `i` and greater than zero, and this is a trivial proof in many cases (e.g. in `factorialEx`). However, having to specify that `i` counts down is still uselessly obscure to the beginner.  
> **username_1** (2023-07-24): @user253751 Thanks. The basic idea is that it might be trivial enough for an algorithm to deduce it on its own. And in the cases where it can’t, and asks the programmer to write a proof, the proof language can be as close to the HLL as possible: the proof is, writing out the function that counts down.  
---
### Answer by username_12 on 2023-07-23. Score: 5
While it is not possible to solve this problem in general (see the halting problem) it is certainly possible to solve it in some very common cases.
For example, in C# if you enter this:
var i = 0;
while (i < 10) {
    Console.WriteLine(i);
}

The editor will put a wiggly line under the while condition and warn that "this condition is always true." FWIW, I'd prefer it considered it an actual error, but that is beside the point. In the specific case you mention it is certainly solvable.
The data flow analysis of the compiler can determine which variables can be changed and in what part of the code. Here is is relatively simple since the variable is local, and so has visibility only in the block, and the parameter passed to Console.Writeline is pass by value. It is certainly possible to do it at a larger scale by tracing what functions can change what variables. For example if this was a property of a class, if private you can readily determine which methods in the class can change that property, since they are the only ones that have access to it.
In languages like C++ this ability is enhanced by the use of const correctness, where the programmer can explicitly specify to the compiler (and the compiler can enforce) these types of rules, enhancing the ability of the dfa to detect this sort of thing.
So it can be done, and it often is done, for many of the most common cases. It can't be done for all cases, and it is harder in lower level languages like C++ where references to variables and aliases can rather easily be hidden, especially if the programmer isn't careful about their const correctness. In these cases the compiler will still produce correct code, just that it'll be more conservative, and more of the "common cases" I mentioned will be considered indeterminable.
I'm not a Python guy, but for sure Python COULD do this too. If it doesn't I'd consider that a shortcoming in the compiler or interpreter you are using.
> **Comments:**
> **username_2** (2023-07-24): I would not recommend making this an actual error because there is more stuff to understand before you can understand the error. The beginner may not understand why the error is there, without reading a bunch of theory - until he actually runs the program and it loops forever, and then he will *instantly* understand it. The epiphany can't happen if you stop him from running the program.  
> **username_13** (2023-07-24): Aside from that, it's useful to be able to write programs that don't offer an explicit exit.  
> **username_12** (2023-07-25): @KarlKnechtel that's an excellent point. There is the classic for(;;) C idiom. But for sure I'd upgrade it to a warning at least.  
---
### Answer by username_14 on 2023-08-04. Score: 2
Simplest check that some languages are already doing is to see if any variables involved in the loop condition check are modified, or otherwise if any break or return statement exists in the loop.

While this is not always (reading from the default input stream would change the loop condition without modifying any visible variables), this would catch majority of errors.
---
