return in loop for ?

[Paul Rubin]

Mike Meyer <mwm at mired.org> 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/