Turing proved with his halting theorem (There's a nice simple proof here) that there is not a correct program $$Halt(p, i)$$ that returns true if program p halts on input i, and returns false if the program does not halt (i.e. if it loops forever). (This is for Turing-complete languages, i.e. languages with programs that may loop forever). However, what does exist, is a correct program HaltM (short for Halt Maybe), that returns one of 3 options: Halts, Unknown, or DoesNotHalt. To show that such a program does exist, we can do a proof-by-construction. Here's the first example of such a program:

HaltM_1(p, i): 
   return Unknown

This program just always returns Unknown regardless of the input. Admittedly that's pretty lame :) To make a slightly more interesting HaltM program, first let's introduce two programs, one which halts on all inputs, one which loops forever on all inputs.

HaltsOnAll(x):  
   return 1

LoopForever(x):  
   Loop Forever

Now we can define a slightly more interesting HaltM program, that doesn't always return Unknown:

HaltM_2(p, i): 
   if p == HaltsOnAll then
      return Halts
   else if p == LoopForever then
      return DoesNotHalt
   else
      return Unknown
   end

What was the point of this proof? I get the feeling that some people seem to think that for Turing-complete languages, it's impossible to say anything about if the program halts or not, just by examining it. This simple counterexample shows, that although you can't write a program Halt(p, i) that can decide for sure in all cases, you can write a program HaltM_2(p, i) that can tell if the program halts or does not halt in some cases.