Saying "latently-typed language" is making a category mistake
pats at acm.org
Fri Jun 23 23:08:39 CEST 2006
Chris Smith wrote:
> 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.
Of course, we can, and should, prefer programs we can prove terminate.
Languages can make it easier or harder to write provably terminating
More information about the Python-list