Chris Uppal wrote: > Pascal Costanza wrote: > > > Sorry, obviously I was far from being clear. ACL2 is not > > Turing-complete. All iterations must be expressed in terms of > > well-founded recursion. > > How expressive does that end up being for real problems ? I mean obviously > in > some sense it's crippling, but how much of a restiction would that be for > non-accademic programming. Could I write an accountancy package in it, or an > adventure games, or a webserver, with not too much more difficulty than in a > similar language without that one aspect to its type system ? > > Hmm, come to think of it those all hae endless loops at the outer level, with > the body of the loop being an event handler, so maybe only the handler should > be required to guaranteed to terminate.
An example of a non-Turing-complete language (at least the core language; the standard is getting huge) with guaranteed termination, that is used everywhere and quite useful, is SQL. I wouldn't want to write an accounting package in it; its abstraction facilities are too weak. But the language is much more powerful than it is usually given credit for. Marshall -- http://mail.python.org/mailman/listinfo/python-list
