From: Frank Stuart <fstuart@vetmed.auburn.edu>
Date: Mon, 9 Oct 95 23:39:54 PDT
To: cypherpunks@toad.com
Subject: [NOISE] was Re: java security concerns
Message-ID: <199510100639.BAA19818@snoopy.vetmed.auburn.edu>
MIME-Version: 1.0
Content-Type: text/plain



This is a bit off-topic, but hopefully interesting.

Rather than trying to prove a program to be correct (which I agree is doomed
to failure for the forseeable future for all but trivial programs), perhaps
it would be useful to have an automated therom-prover to try to deduce
"interesting things" about certain programs such as "this program always
bounds-checks its input", "this program allows writes to arbitrary files on
lines x, y, and z", "this program halts". (:>)  Obviously (as the last example
illustrates), this isn't perfect because something can be true without being
provable.  Further, it's likely that assumptions must be made about system
calls, libraries, and the ways in which they interact.  There's also the
problem of "who proves the prover".  However, I think such a tool would be
useful because it may quickly point out things not obvious to (most) humans
and getting some idea of what can't be deduced and why would be instructive.


                          | (Douglas) Hofstadter's Law:
Frank Stuart              | It always takes longer than you expect, even 
fstuart@vetmed.auburn.edu | when you take into account Hofstadter's Law.