How difficult is software? [Re: OVC-discuss Digest, Vol 37, Issue 18]

From: Hamilton Richards <hrichrds_at_swbell_dot_net>
Date: Wed Nov 14 2007 - 09:58:48 CST

As Danny Swarzman observes, "software isn't witchcraft." Indeed,
it's pure logic, applied on a large scale. (I say so from the vantage
point of a 40-year career devoted to practicing that applied logic
and teaching it to college students.)

It's probably true that "an ordinary person can figure it [i.e.,
software] out", if "figure it out" means "get a rough idea of what a
program means, and maybe cobble together a program that seems to
work."

There is, however, a *huge* gulf between (1) reading and writing
software and (2) verifying software.

As evidence, consider the software produced by the many "people who
use computer languages such as Java and xml." Such hard-working and
well-meaning folks are the ones who produce the vast majority of the
software sold around the world. With almost no exceptions, that
software comes with blanket disclaimers which, translated from
legalese, absolve the vendors of all responsibility for their
products' correct operation.

Can you name another industry that has such abysmal standards--and
gets away with it?

If "ordinary people" can observe hand counting of ballots, then they
outnumber those who can verify open-source software by many orders of
magnitude.

At this point you may be suspecting that what Mr Swarzman means by
"verify" and what I mean by it are two quite different notions. I
don't wish to put words in his mouth, but in commonplace
software-industry usage, "verify" means something like "inspect the
source code, and test the corresponding executable until the rate of
error discovery drops to some acceptable level." Even if the
"acceptable level" is zero, however, testing cannot ensure that the
software is error-free--for any program that is not utterly trivial,
the number of cases to be tested makes exhaustive testing impossible.
As Edsger W. Dijkstra famously said, "program testing may
convincingly demonstrate the presence of bugs, but can never
demonstrate their absence"
<http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html>.

Inspection is actually more promising, but the way it is commonly
practiced is far from adequate. It usually amounts to no more than
some combination of line-by-line scrutiny and mental execution. As
evidence of its inadequacy, consider the phenomenon of "Easter eggs".
In software, an Easter egg is a hidden feature--often a spectacular
one--inserted by the programmers as a kind of joke, and as evidence
of their creativity and cleverness
<http://en.wikipedia.org/wiki/Easter_egg_(virtual)>. Many software
companies have stringent policies against Easter eggs and hunt them
down mercilessly, yet they continue to appear.

To be effective, inspection must rise to the level of formal
reasoning <http://en.wikipedia.org/wiki/Formal_verification>, i.e.,
mathematical proofs that programs satisfy given (formal)
specifications. Such formal methods have been used successfully in
developing commercial hardware and software since at least as far
back as 1985, and their use has been spreading gradually
<http://vl.fmnet.info/companies/>, but it's still far from the norm.

If someone is seriously contemplating the application of such formal
methods to software used in elections, I say more power to them, but
I'm not holding my breath.

All the best,

--Ham

At 12:00 PM -0800 2007/11/13, ovc-discuss-request@listman.sonic.net wrote:
>[...]
>Message: 1
>Date: Mon, 12 Nov 2007 19:39:32 -0800
>From: Danny Swarzman <danny@stowlake.com>
>Subject: [OVC-discuss] Is hand count transparent?
>To: Open Voting Consortium discussion list
> <ovc-discuss@listman.sonic.net>
>Message-ID: <EC3797E4-18E3-4152-8DC0-4DE7D1117C9B@stowlake.com>
>Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
>
>[...]
>
>But, software isn't witchcraft. An ordinary person can figure it out.
>There are a lot of people who use computer languages such as Java and
>xml. There' a huge number of books on these subject.
>
>If you don't want to read source code, you can get the source code
>from the internet and follow directions and set up your own elections
>system. Print some ballots. scan some votes see who wins in your world.
>
>Like any human document, source code can be written clearly or not.
>We hope ours is.
>
>There is a lot of talk about how difficult software is. Complex
>software is tough to get completely correct in every detail. But this
>isn't that complex. The source code involved is small compared to the
>documents that describe the applicable regulations.
>
>Do you really think there is a larger class of people who can
>observer hand counting than there is who can verify open source
>software? They weren't in City Hall last Tuesday round midnight.
>
>-Danny

-- 
------------------------------------------------------------------
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
By sending email to the OVC-discuss  list, you thereby agree to release the content of your posts to the Public Domain--with the exception of copyrighted material quoted according to fair use, including publicly archiving at  http://gnosis.python-hosting.com/voting-project/
==================================================================
= The content of this message, with the exception of any external 
= quotations under fair use, are released to the Public Domain    
==================================================================
Received on Fri Nov 30 23:17:23 2007

This archive was generated by hypermail 2.1.8 : Fri Nov 30 2007 - 23:17:31 CST