Saying "latently-typed language" is making a category mistake
cdsmith at twu.net
Fri Jun 23 17:19:51 CEST 2006
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
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
More information about the Python-list