Re: Microsoft-backed Consortium, AeA, Opposing Open Voting Bill, AB 852 (Richard C. Johnson)

From: Richard C. Johnson <dick_at_iwwco_dot_com>
Date: Fri Apr 27 2007 - 11:57:33 CDT

                      
Mr. Richards,

I actually believe that Open Source and Open Test
supplement, embody, and perfect the techniques of
inspection and test, none of which will ever result
in something perfectly correct.

>No kidding. I think you're misreading "is capable of
>operating correctly" as "always operates correctly". No. I was referring to the statement “Inspecting and
testing software can show that it is capable of operating
correctly” as untrue because I believe that it is never
possible for inspection and testing to lead to the
conclusion that software “works correctly.” You later
seem to agree with that, if I understand you correctly. >If a piece of software passes any tests at all, you've
>shown that under some conditions it can operate correctly. No. This is only true if it is also trivial. No
inspection (which is always incomplete) and no testing
(which is also incomplete) ever “proves” anything other
than that something does not work which fails the test
(even then, the test may be faulty). The assumption
that a passed test proves any degree of correctness
(why do you think tests are repeated and regression
tests prized?) is mere hubris. I have myself been
guilty of this faulty reasoning and have supervised
software engineers who shared in it. It is a common
fault; no real world engineer with much experience
would rest correct operation on “any test at all.” >On the other hand, even if the software passes every
>test you give it, you can't possibly have given it
>every possible test (unless the software is utterly
>trivial), and you can never know whether one of >the vast number of tests you omitted would have
>caused the software to fail. So you can't (in finite
>time) show that the software is incapable of giving
>an incorrect result. Yes, you are starting to get it, although you have only
gone part of the way. No finite set of test exhausts
possible failures, and I would venture to guess that
no infinite set of tests (constructed by mortals) would
do so, either. Barking up the wrong tree is ineffective
even for infinite barks. It is also true that no one
I know ever has ever believed in perfect software or
anything close to it. Reliable, well tested, thoroughly
inspected, useful in practice are all goals with which
I am familiar. >I have always agreed that testing and inspection can
>improve code's quality. That, however, is not the same
>as a guarantee that it will operate correctly in all cases. Yes. But this is a straw man argument. No rational
engineer of my acquaintance expects anything to “operate
correctly in all cases.” Whom do you know who believes
in invariable, immutable correctness for real code? It is
enough for commercial code that the vendor does diligent
inspection and test. For very important code, various
parties with different points of view should be able to
see, inspect, and test the code. This is Open Source.

>That truism holds for empirical sciences, but not for
>computing science --which is really a branch of applied
>mathematics. In mathematics --and in computing science--
>it is indeed possible to prove theories true. In my
>undergraduate classes at UT, proving the correctness
>of code was a routine exercise. For more on the subject, >a good starting place might be [1]. Hmmm. Do you believe? Maybe a few lines of code can be
reduced to a tautology, or a logical thread expressed in
an algorithm (of limited size) may be subject to
mathematical proof. But no serious, relevant, real life
code with committee-originated requirements can ever be
shown to be “correct” by mathematical legerdemain except
if the requirements themselves are “correct.” Then,
“correct by construction” applies.

I hope that your students who find employment understand
that in the outside world, requirements are seldom if
ever this neat and well defined. It might be good for
you to re-read the Wikipedia piece you cited, in which
it is stated that formal methods are a bit expensive.
Algorithms perhaps, but not applications, and not in the
real world.
 
So...for all practical purposes, the truism I cited
goes beyond the physical sciences to affect computer
engineering and computer programs simply because
mathematical models cannot and do not fit the real
world requirements against which software bugs are
declared. Diligent and intelligent inspection and
testing, according to a well-planned and well-executed
test plan, are all we have. For something as important
as voting, whose eyes inspect and what tests are run
is a matter of public concern. Only Open Source and
Open Test allow the community to see and to judge.
 
That is the reason I am drawn to Open Source as the
best solution in an imperfect and marginally correct
world.
Sincerely,

Dick Johnson

 

Hamilton Richards <hrichrds@swbell.net> wrote: >Message: 2
>Date: Thu, 26 Apr 2007 05:48:41 -0700 (PDT)
>From: "Richard C. Johnson"
>Subject: Re: [OVC-discuss] Microsoft-backed Consortium, AeA, Opposing
> Open Voting Bill, AB 852
>To: Open Voting Consortium discussion list
>
>Message-ID: <75845.64581.qm@web402.biz.mail.mud.yahoo.com>
>Content-Type: text/plain; charset="iso-8859-1"
>
>Mr. Richards,
>
>The key point in your argument seems to be:
>
> Inspecting and testing software can show that it is capable of
> operating correctly, but can never show that it is incapable
> of operating incorrectly.
>
> I disagree that this is the traditional wisdom in the software
>business, and I would argue that the above is simply false. No
>amount of inspecting and testing catches all bugs, in my experience.

No kidding. I think you're misreading "is capable of operating
correctly" as "always operates correctly".

>Rather I have always understood the saying as:
>
> Inspecting and testing software can prove that it is NOT capable of
> operating correctly, but can never prove that it is capable of
> operating correctly in all instances called for in the specification.

Well, that's closer to Dijkstra's well-known statement of the idea
(although he referred only to testing, not inspection), but mine is
equivalent.

> You had it backwards.

I don't think so. Consider:

If a piece of software passes any tests at all, you've shown that
under some conditions it can operate correctly. Every test that it
passes expands the conditions under which it operates correctly. So
testing software can show that it is capable of operating correctly.

On the other hand, even if the software passes every test you give
it, you can't possibly have given it every possible test (unless the
software is utterly trivial), and you can never know whether one of
the vast number of tests you omitted would have caused the software
to fail. So you can't (in finite time) show that the software is
incapable of giving an incorrect result.

>A confirmed bug means that something does NOT work. The absence of
>a reported or confirmed bug does NOT mean that something works, only
>that it may not be in use, the users are too lazy to report bugs,
>the testing was inadequate, and so on. The logic is that, for the
>statement a > b, -b (a bug) implies -a, but -a implies nothing. For
>a scientist, this is the truism that you can always falsify a
>theory, but you can never prove one true (theories are only
>supported and not proven by empirical evidence).

That truism holds for empirical sciences, but not for computing
science --which is really a branch of applied mathematics. In
mathematics --and in computing science-- it is indeed possible to
prove theories true. In my undergraduate classes at UT, proving the
correctness of code was a routine exercise. For more on the subject,
a good starting place might be [1].

>What you want is code that has been subjected to risk of failure,
>has had much testing (with disclosure of results) and is open to
>review by a wide variety of professionals and skilled amateurs.
>Test coverage, another interesting traditional requirement for
>assessing the likelihood that code will perform as expected, is
>another topic.

I have always agreed that testing and inspection can improve code's
quality. That, however, is not the same as a guarantee that it will
operate correctly in all cases.

>For Open Source, the belief is that public scrutiny of code by
>technical peers (community inspection and experience) produces safer
>and more reliable code than the commercial process, with its
>frequent skipping of testing and its willingness to ship code that
>worked in just a few instances. Your flawed argument is not enough
>to disabuse anyone here of the notion that Open Source leads to
>better, more reliable code. In my humble opinion.

Well, that "flawed argument" was never *my* argument. As you will see
if you go back and read my posting again, when you have time to read
it more carefully.

By the way, I've long been convinced of the benefits of Open Source,
but I hold this view as a considered opinion, not a religious belief.
In particular, I don't see any evidence that Open Source overcomes
the limitations of inspection and testing.

All the best,

--Ham

1.

-- 
------------------------------------------------------------------
Hamilton Richards, PhD           Department of Computer Sciences
Senior Lecturer (retired)        The University of Texas at Austin
ham@cs.utexas.edu                hrichrds@swbell.net
http://www.cs.utexas.edu/users/ham/richards
------------------------------------------------------------------
_______________________________________________
OVC-discuss mailing list
OVC-discuss@listman.sonic.net
http://lists.sonic.net/mailman/listinfo/ovc-discuss

_______________________________________________
OVC-discuss mailing list
OVC-discuss@listman.sonic.net
http://lists.sonic.net/mailman/listinfo/ovc-discuss

==================================================================
= The content of this message, with the exception of any external
= quotations under fair use, are released to the Public Domain
==================================================================
Received on Mon Apr 30 23:17:15 2007

This archive was generated by hypermail 2.1.8 : Mon Apr 30 2007 - 23:17:17 CDT