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/ -- http://mail.python.org/mailman/listinfo/python-list
