Saying "latently-typed language" is making a category mistake
Patricia Shanahan
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
> 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.
>
Of course, we can, and should, prefer programs we can prove terminate.
Languages can make it easier or harder to write provably terminating
programs.
Patricia
More information about the Python-list
mailing list