Mike Meyer <[EMAIL PROTECTED]> writes: > >> Which means you can't create a verifier which will verify all > >> programs. Is there a reason to believe that you can't have a verifier > >> with three possible outcomes: Correct, Incorrect, and I don't know, > >> and it is always correct in doing so? Note that "I don't know" could > >> be "I ran longer than I think is reasonable and gave up trying." > > It's trivial to write such a verifier, if you get my drift. > > Almost as cute as the simplest self-replicating shell script. > > Ok, so it's possible. Are there any useful examples? Does the BCPL > type verifier count?
The trivial verifier simply prints "I don't know" for EVERY program you input. It is never wrong. I don't know about the BCPL type verifier but every statically typed language verifies certain assertions about the types of expressions and this is useful. I think I heard that the Hindley-Milner algorithm always succeeds (not sure what the conditions are for that) but that it can take exponential time for some pathological cases. The incompleteness theorem says there are undecidable problems in any system complex enough to include Peano arithmetic. So if the Hindley-Milner algorithm always succeeds, it just means that type systems aren't complex enough to express arithmetic in. I don't really know enough about this type stuff to discuss it sensibly at the moment. There's a book I want to read, "Types and Programming Languages" by Benjamin Pierce, which is supposed to explain it pretty well. It's supposed to be excellent. But I haven't had a chance to sit down with a copy yet. http://www.cis.upenn.edu/~bcpierce/tapl/ -- http://mail.python.org/mailman/listinfo/python-list
