"Diez B. Roggisch" <[EMAIL PROTECTED]> writes: > All serious languages are turing-complete. So can we put away with this > non-sense argument right away, please?
Actually the so called "total" languages aren't Turing-complete. I think Coq is an example: every Coq function must return a value. So Coq doesn't have any way to write an infinite loop, because that would allow writing functions that fail to return. So there is no halting program in Coq (every Coq program halts), which means Coq is not Turing-complete. That allows Coq to generate code about which it can make all kinds of guarantees that most languages can't (not simply that the programs halt but that they actually fulfill their computational specifications), so it's being used in various high-assurance applications, though usually to write just the most critical parts of a program, not the entire program. Of course it's a matter of semantics but in some meaningful ways, I'd say Coq is a more serious language than Python. Here is a famous early paper explaining why Turing-completeness isn't all it's cracked up to be: http://sblp2004.ic.uff.br/papers/turner.pdf This paper shows some of the advantages of the total approach. -- http://mail.python.org/mailman/listinfo/python-list
