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

[Matthias Blume]

Pascal Costanza <pc at p-cos.net> writes:

> Patricia Shanahan 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.
>
> Not quite. See http://en.wikipedia.org/wiki/ACL2

What do you mean "not quite"?  Of course, Patricia is absolutely
right.  Termination-guaranteeing languages are fundamentally less
expressive than Turing-complete languages.  ACL2 was not mentioned in
the newsgroup header.