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

[Pascal Costanza]

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


Pascal

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