[racket] Checking infinite loops

Patrick, in principle you're not mistaken to ask for a 'loop checker'. 
Many people work on this topic -- despite the Halting Problem -- to this
day, mostly in language contexts that are connected to theorem proving 
(or logic programming, which is close). 

If you're really interested, start with the ACL2 theorem prover. Its
syntax is reminiscent of Racket's thought it is first-order. Before 
ACL2 deals with any (Racket-like) function definition, it proves that
the function terminates (produces a result) for all possible inputs. 
If it can't, it won't accept the function definition. The programmer
can then supply a 'hint' on why he thinks the function should terminate. 

Dealing with this topic, you will quickly discover extremely deep 
connections between logic and computing. Even in ACL2 for example, 
you're on occasion forced to use transfinite ordinals and induction to 
spell out the reasoning behind a termination argument. But that's just
the beginning. There is much more once you get into it. 

So the question causes general laughter in some quarters, but in a way
it is an extremely relevant question to ask in modern days though it's 
not asked for the most common languages. 

-- Matthias