return in loop for ?

[Steven D'Aprano]

Re: return in loop for ?

On Mon, 28 Nov 2005 08:44:04 +0000, Duncan Booth wrote:
[color=blue]
> Steven D'Aprano wrote:
>[color=green]
>> Since real source code verifiers make no such sweeping claims to
>> perfection (or at least if they do they are wrong to do so), there is
>> no such proof that they are impossible. By using more and more
>> elaborate checking algorithms, your verifier gets better at correctly
>> verifying source code -- but there is no guarantee that it will be
>> able to correctly verify every imaginable program.
>>[/color]
> I'm sure you can make a stronger statement than your last one. Doesn't
> Godel's incompleteness theorem apply? I would have thought that no matter
> how elaborate the checking it is guaranteed there exist programs which are
> correct but your verifier cannot prove that they are.[/color]

Yes, of course. By saying "no guarantee" I was guilty of understatement:
at the very least, we can guarantee that the verifier will *not* correctly
verify every possible program. (Which of course is no different from human
programmers.)

--
Steven.

[Steven D'Aprano]

Re: return in loop for ?

On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote:
[color=blue]
> Duncan Booth enlightened us with:[color=green]
>> I would have thought that no matter how elaborate the checking it is
>> guaranteed there exist programs which are correct but your verifier
>> cannot prove that they are.[/color]
>
> Yep, that's correct. I thought the argument was similar to the proof
> that no program (read: Turing machine) can determine whether a program
> will terminate or not.[/color]

No, that is not right -- it is easy to create a program to determine
whether *some* programs will terminate, but it is impossible to create a
program which will determine whether *all* programs will terminate.


--
Steven.

[Mike Meyer]

Re: return in loop for ?

Steven D'Aprano <steve@REMOVETH IScyber.com.au> writes:[color=blue]
> On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote:[color=green]
>> Duncan Booth enlightened us with:[color=darkred]
>>> I would have thought that no matter how elaborate the checking it is
>>> guaranteed there exist programs which are correct but your verifier
>>> cannot prove that they are.[/color]
>> Yep, that's correct. I thought the argument was similar to the proof
>> that no program (read: Turing machine) can determine whether a program
>> will terminate or not.[/color]
> No, that is not right -- it is easy to create a program to determine
> whether *some* programs will terminate, but it is impossible to create a
> program which will determine whether *all* programs will terminate.[/color]

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."

<mike
--
Mike Meyer <mwm@mired.or g> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Mike Meyer]

Re: return in loop for ?

Paul Rubin <http://phr.cx@NOSPAM.i nvalid> writes:[color=blue]
> Mike Meyer <mwm@mired.or g> writes:[color=green]
>> 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."[/color]
> It's trivial to write such a verifier, if you get my drift.[/color]

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?

<mike
--
Mike Meyer <mwm@mired.or g> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Steven D'Aprano]

Re: return in loop for ?

On Mon, 28 Nov 2005 12:05:03 -0500, Mike Meyer wrote:
[color=blue]
> Steven D'Aprano <steve@REMOVETH IScyber.com.au> writes:[color=green]
>> On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote:[color=darkred]
>>> Duncan Booth enlightened us with:
>>>> I would have thought that no matter how elaborate the checking it is
>>>> guaranteed there exist programs which are correct but your verifier
>>>> cannot prove that they are.
>>> Yep, that's correct. I thought the argument was similar to the proof
>>> that no program (read: Turing machine) can determine whether a program
>>> will terminate or not.[/color]
>> No, that is not right -- it is easy to create a program to determine
>> whether *some* programs will terminate, but it is impossible to create a
>> program which will determine whether *all* programs will terminate.[/color]
>
> Which means you can't create a verifier which will verify all
> programs.[/color]

I thought that's what I said originally *wink*
[color=blue]
> 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."[/color]

That seems perfectly reasonable to me.

I don't know about anyone else in this discussion, but I'm talking about
*theoretical* source code verification of formal correctness. In
*practice*, I don't know what the state of the art is, but I suspect it
will be a long, long time before it is as easy as running "import
mymodule; verify(mymodule )".


--
Steven.

[Paul Rubin]

Re: return in loop for ?

Mike Meyer <mwm@mired.or g> writes:[color=blue][color=green][color=darkred]
> >> 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."[/color]
> > It's trivial to write such a verifier, if you get my drift.[/color]
>
> 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?[/color]

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/

[Paul Rubin]

Re: return in loop for ?

Steven D'Aprano <steve@REMOVETH IScyber.com.au> writes:[color=blue]
> I don't know what the state of the art is, but I suspect it
> will be a long, long time before it is as easy as running "import
> mymodule; verify(mymodule )".[/color]

Some pretty significant pieces of software have been formally verified
to meet their formal specifications. The trouble with
"verify(mymodul e)" is that usually means something closer to "verify
that mymodule does what I hope it does". The computer does not yet
have a telepathy peripheral that can read your mind and figure out
what you are hoping, and people's attempts to express formally what
they are hoping are easily wrong just like programs are often wrong.

[Mike Meyer]

Re: return in loop for ?

Paul Rubin <http://phr.cx@NOSPAM.i nvalid> writes:[color=blue]
> 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.[/color]

BCPL is untyped. You can perform any operation on any variable. You
can use the floating point add op on a pair of ints, or a pair of
function pointers. It doesn't care - it doesn't know what types the
variables are.

The type verifier extracted type information from context, and
propogated that through the system to look for places where the
programmer applied an operation to a type for which it was
inappropriate. It found bugs in itself.
[color=blue]
> 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.[/color]

I've been looking through it. It deals with type correctness, and by
association, evalulation completion. There are some fairly complex
systems in it. He does promise to reveal the features of programming
languages that cause the programs (or their type validation) to fail
to terminate.

<mike
--
Mike Meyer <mwm@mired.or g> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Alex Martelli]

Re: return in loop for ?

Paul Rubin <http://phr.cx@NOSPAM.i nvalid> wrote:
[color=blue]
> Steven D'Aprano <steve@REMOVETH IScyber.com.au> writes:[color=green]
> > I don't know what the state of the art is, but I suspect it
> > will be a long, long time before it is as easy as running "import
> > mymodule; verify(mymodule )".[/color]
>
> Some pretty significant pieces of software have been formally verified
> to meet their formal specifications. The trouble with
> "verify(mymodul e)" is that usually means something closer to "verify
> that mymodule does what I hope it does". The computer does not yet
> have a telepathy peripheral that can read your mind and figure out
> what you are hoping, and people's attempts to express formally what
> they are hoping are easily wrong just like programs are often wrong.[/color]

Yep. I'm reminded of an ambulance dispatch system (read about it a long
time ago on the Risks mailing list, so I might be off on the detail, but
the gist should be correct) which was formally proven to obey a long
list of rules, one of which was "for this kind of emergency, an
ambulance must arrive within 10 minutes" (or the like).

Problem, of course, being that in formal logic this implies "if this
kind of emergency exists and no ambulance has arrived within 10 minutes,
you have an impossibility and from an impossibility ANY theorem can be
proven". So, if real-world road conditions meant the ambulance was
about to arrive in 10 minutes and 5 seconds, it might instead be
rerouted elsewhere... not having arrived in 10 minutes, a contradiction
was in the system and it could prove anything (I think that's know as
the theorem of Pseudo-Scotus). It's hard in (classic) logic to express
"this MUST be true; if it's false, ..." -- to human beings the first
"MUST" can be interpreted as "99.9% probability" or the like, so the "if
it's false" clause is meaningful ("in the extremely unlikely, but not
impossible since nothing's truly impossible in the real world, situation
that it's false, ..."), but to Aristotle's logic, if something MUST be
true, it's obviously irrelevant whatever might follow if that something
were instead to be false.


Alex