Email thread begun by Shankar, Fri, 13 Aug 2010 16:44:33 -0700 [and
continued as indicated.]

Matt: The notes are very detailed -- it's impressive and scary that you
can type that fast.   We should perhaps collapse it into something more
digestible.

Larry's point about trust for whom (power users, novices, malicious
users) is important.  The latter class is basically irrelevant since
there are simple mechanisms to rule this out.  

  [From Matt 14 Aug: What do you mean by "simple mechanisms"?  For
  example, if a malicious user knew of some obscure soundness bug in
  ACL2, that could be used to give a bogus correctness proof; but it
  might be far from simple to know of this bug, let alone to find that
  it's been exploited.]

  [From Rob 21 Aug: See comment on "malicious subversion" in
  rob-arthan-08-21.txt.]

The point about the trusted base vs. trustworthiness is worthy of
clarification.

  [From Matt 14 Aug: Please let me know if there anything specific
  below that you suggest needs such clarification.]

On warranties, this is a very slippery slope.  Verification deals with a
very narrow, though important, sliver of the problem.  You don't want to
encourage implementors to pass on the blame to you for their crappy
products just because you're willing to offer a warranty.  

  [From Larry 14 Aug:

  Forgive me if I repeat my usual line concerning warranties. Software
  is perhaps the only product in the world that gives the purchaser no
  rights at all. They can discover that their software will not launch
  without having the right to a refund or even the right to resell the
  software. And yet a new computer, an immensely complicated and
  sophisticated artefact, comes with full warranty rights.

  Naturally I don't expect to see ordinary consumer software becoming
  verified in my lifetime, but we should be striving to raise the
  issue of warranties and consumer rights in order to force software
  developers to improve their methods. They can begin by using safer
  languages and thorough static checking. I hope this will prove to be
  a slippery slope that puts an end to crappy development practices,
  even if our particular methods may only become relevant at the
  bottom of the slope.
  ]

  [From Rob 21 Aug: See comment on warranties in rob-arthan-08-21.txt.]

On soundness, it is very important for many reasons, the least of which
is that the final result can be believed.  Inference is used in many
ways, e.g., for simplification, invariant generation, guard checking,
compiler optimization/parallelization.  Many of these are not about
producing QED, but soundness is still of value.  These are applications
where no one really cares if there is a proof object - you have to do it
right because it saves a lot of hassle.  I did a few modest PVS proofs
on the train journey to Edinburgh, and my failed attempts to prove the
TCCs quickly caught several fairly deep bugs.  Without PVS, I'd be in a
Persistent Vegetative State.

  [From Matt 14 Aug: Regarding "Burkhart's point" mentioned below, to
  which of his four comments do you refer?]

Burkhart's point about truth prevailing (not exactly what he said, but
possibly, what he meant) is a good one.  This is the Indian motto, but
it hasn't done much for India.  If anything, both within India and
without, the untruthful have prevailed and the meek have not inherited
the earth.  Unfortunately, there is very little evidence to support it
in religion, politics, or even science.  Dijkstra's THE operating system
was an amazing accomplishment and his ideas did have an impact, but the
products that prevailed were all tangential to the truth.  In fact, our
story should not be that we're striving for truth, but that we're doing
something useful, and soundness, among other things, is pretty useful.

The reliability through diversity argument is also important.  Using
multiple computer algebra systems does not guarantee reliability since
they can easily have correlated failures, but using some kind of
majority vote is a good way to find bugs.  John Rushby's work on
"possible perfection" shows one way that verification can contribute to
orthogonal diversity.

Mike's "nimbleness" point is critical, as are J's points about
formalization, modeling, and validation.  We don't just need to trust
the inferences, but we also have to develop trust in and through our
formalizations.

George's point about semantics is also important.  Why are we proving
theorems if we they can't be used other than by someone parked inside
the theorem proving system?  This is another reason why I think it's a
good idea to think in terms of embedding theorem provers within other
systems so that we get out of this "logocentric predicament".

I realize that my opinions might not be shared by others at the
workshop, but as my dad always advised me, the truth is somewhere in
between.

-Shankar

============================================================