Saying "latently-typed language" is making a category mistake

[Chris Smith]

Patricia Shanahan <pats at acm.org> wrote:
> Vesa Karvonen wrote:
> ...
> > An example of a form of informal reasoning that (practically) every
> > programmer does daily is termination analysis.  There are type systems
> > that guarantee termination, but I think that is fair to say that it is not
> > yet understood how to make a practical general purpose language, whose
> > type system would guarantee termination (or at least I'm not aware of such
> > a language).  It should also be clear that termination analysis need not
> > be done informally.  Given a program, it may be possible to formally prove
> > that it terminates.
> 
> To make the halting problem decidable one would have to do one of two
> things: Depend on memory size limits, or have a language that really is
> less expressive, at a very deep level, than any of the languages
> mentioned in the newsgroups header for this message.

Patricia, perhaps I'm misunderstanding you here.  To make the halting 
problem decidable is quite a different thing than to say "given a 
program, I may be able to prove that it terminates" (so long as you also 
acknowledge the implicit other possibility: I also may not be able to 
prove it in any finite bounded amount of time, even if it does 
terminate!)

The fact that the halting problem is undecidable is not a sufficient 
reason to reject the kind of analysis that is performed by programmers 
to convince themselves that their programs are guaranteed to terminate.  
Indeed, proofs that algorithms are guaranteed to terminate even in 
pathological cases are quite common.  Indeed, every assignment of a 
worst-case time bound to an algorithm is also a proof of termination.

This is, of course, a very good reason to reject the idea that the 
static type system for any Turing-complete language could ever perform 
this same kind analysis.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation