Testing, testing, one to three, testing

Imagine the brain of a software developer in which the left hemisphere
is devoted to pragmatism and the right hemisphere is devoted to
intellectual rigor and correctness. Let's travel through that brain,
surfing on a wave of thought, from left earlobe to right earlobe. The
thought we are surfing on is this: "How do I know my software is
correct?".

As we travel from left to right, neurons fire in all directions. Out of
the synaptic snowstorm that ensues, three answers solidify from
different sectors of the brain. They are, in order:

Sector 1 Answer: Working software is software that gets the job done
before my boss fires me.

Sector 2 Answer: Working software is software that passes all my tests
including the test of time. (i.e. not only has it passed all the tests
I have put it through but it has been running error free for a long
time.)

Sector 3 Answer: Working software is software that I can prove to be bug
free using a formal, mathematical theorem proving mechanism.

As an industry, we have spent a lot of time in sector 1. Software
development, especially commercial software development, is a high
pressure activity in which engineering requirements need to be traded
off with a heady concoction of requirements from other aspects of the
business. We need to get the stuff to work before the customer walks
down to our competitors, before the boss blows a gasket and so on.

As software development has matured over the years, we have codified
more and more best practice. This best practice lore is pushing us more
and more towards sector 2. This is good. Anything is better than the
'ship it, then worry', realities of sector 1.

Few would argue that in an ideal world, the science of computer science
would allow us to skip the empirical world of sector 2 and head straight
for the logical nirvana of formal correctness over in sector 3. After
all, as Edsgar Dijkstra famously observed, testing can only show the
*presence* - but not the *absense* of bugs. We can never say that we
know our software works, we can only say that, so far, we have failed to
show that it does not.

Personally, I think we will stay in sector 2 for a long, long time.
Perhaps even for ever. You don't need to spend much time contemplating
the enormity of the problem of formal correctness to realize that we
have a long way to go to get there. Indeed, we may never get there.
Formal correctness as a field of endeavor appears to have a history akin
to that of artificial intelligence. After a period of considerable
activity and excitement in the mid to late Eighties, activity has died
down and expectations seem to have been lowered as to what can
realistically be achieved.

Sign up for ITworld's Daily newsletter
Follow ITworld on Twitter @IT_world

• Email
• Print
• Share
  • Slashdot
  • Digg
  • Stumble
  • Reddit
  • Newsvine