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

[Pascal Costanza]

Matthias Blume wrote:
> 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.

ACL2 is a subset of Common Lisp, and programs written in ACL2 are 
executable in Common Lisp. comp.lang.lisp is not only about Common Lisp, 
but even if it were, ACL2 would fit.


Pascal

-- 
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/