Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 15 Apr 1994 19:24:23 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA21899; Fri, 15 Apr 1994 12:10:02 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA21895; Fri, 15 Apr 1994 12:09:51 -0600 Received: from bilbo.radonc.washington.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA01270; Fri, 15 Apr 1994 11:10:03 -0700 Received: by violin1.radonc.washington.edu (1.38.193.4/16.2) id AA16902; Fri, 15 Apr 1994 11:10:18 -0700 Date: Fri, 15 Apr 1994 11:10:18 -0700 From: Jon Jacky To: info-hol@cs.uidaho.edu Cc: homeier@cs.ucla.edu In-Reply-To: "peter v. homeier"'s message of Thu, 7 Apr 94 19:41:20 PDT <940408.024120z.19218.homeier@oahu.cs.ucla.edu> Subject: Re: How close is practical program proving? Message-ID: <"swan.cl.cam.:096140:940415182505"@cl.cam.ac.uk> I think this discussion has confused just doing verification with using verification technology. They are not the same thing! Many programmers know about pre- and post-conditions and invariants, and think about them when they write programs. It often helps. Does that not count as "practical program proving"? People have asked why verification is so difficult. In fact, like most things it presents a range of difficulty. Don't forget that some verifications that aren't so difficult would still be a big improvement over what many programmers are now doing, which amounts to guessing followed by trial and error. Today's verification technology is pretty forbidding. I see two main barriers to wider use. First, it is just a whole lot of work to use. All of these systems seem to require months of intense work before you develop enough skill, and can build up (or find out about) enough theory to express anything interesting. Second, it seems to demand a grasp of deep foundational issues that is way out of proportion to the depth of the problems that people usually need to solve. I've enjoyed the last week's discussion of number theory, and I can appreciate the usefulness of automatically proving certain arithmetic formulas, but is it really necessary to know about Presburger arithmetic and Peano axioms to establish simple facts about elementary arithmetic? I think it is important for programmers to understand that doing verification is not the same as using heavy verification technology. Some useful verification can be done without a whole lot of fuss, but things like HOL are out there if you really need them. - Jon Jonathan Jacky jon@radonc.washington.edu Radiation Oncology RC-08 voice: (206)-548-4117 University of Washington FAX: (206)-548-6218 Seattle, Washington 98195 USA