"Strong typing vs. strong testing"

[Paul Rubin]

RG <rNOSPAMon at flownet.com> writes:
> Yes, I know I could have used lint.  But that misses the point.  For any 
> static analyzer, because of the halting problem, I can construct a 
> program that either contains an error that the analyzer will not catch, 
> or for which the analyzer will produce a false positive.

Can you describe any plausible real-world programs where the effort of
complicated static is justified, and for which the halting problem gets
in the way of analysis?  By "real world", I meanI wouldn't consider
searching for counterexamples to the Collatz conjecture to qualify as
sufficiently real-world and sufficiently complex for fancy static
analysis.  And even if it did, the static analyzer could deliver a
partial result, like "this function either returns a counterexample to
the Collatz conjecture or else it doesn't return".  

D. Turner wrote a famous paper arguing something like the above, saying
basically that Turing completeness of programming languages is
overrated:

  http://www.jucs.org/jucs_10_7/total_functional_programming

The main example of a sensible program that can't be written in a
non-complete language is an interpreter for a Turing-complete language.
But presumably a high-assurance application should never contain such a
thing, since the interpreted programs themselves then wouldn't have
static assurance.