On software quality and engineering

[Martin Schwenke]

[Mikal, I'm happy to talk about this at CLUG this month, if there's
 interest.  It has occupied a fair amount of my life...  :-]

[Yep, this is long, but I'll try to only get on my soapbox once...]

>>>>> "Michael" == Michael Bennett <mr_b at tpg.com.au> writes:

    Michael> [...]  There are formal specification languages that can
    Michael> be used to mathmatically prove the specification. Most
    Michael> people don't use them as it takes too much time and more
    Michael> effort when they could be programming. I know some
    Michael> companies now use them for all software projects as they
    Michael> can produce software with zero defects.

Yes, you:

1. Specify your software in a mathematical langauge.

2. Think of some properties that you'd like your system to have and
   write them in the mathematical language.

3. Prove that the specification has the properties.

It does take longer to write the the software, but the maintenance
costs end up substantially lower...  especially if you get yourself a
good proof tool...  :-)

>>>>> "David" == David Gibson <david at gibson.dropbear.id.au> writes:

    David> More to the point, once you put the specifications into a
    David> formal language, it's not clear that it's significantly
    David> easier to tell that the specifications are correct than to
    David> tell that the code is correct.

C'mon!  That depends who you are...  and I know who you are!  :-)  

If you understand the mathematics, it is easier to tell whether a
specification meets the required properties.  However, it may not be
obvious that the properties have been correctly specified.  :-)

>>>>> "Simon" == Simon Fowler <simon at himi.org> writes:

    Simon> Another point is that if you have the specification in that
    Simon> formal language, then you effectively /have/ the code - if
    Simon> the formal language is sufficient to describe the system
    Simon> completely, then it should be equivalent to the code for
    Simon> the system. Equivalent meaning automatically translatable
    Simon> to the code (and hence to the final executable).

No!  Specifications describe "what" a system should do and code
describes "how" it should be done.  The process of transforming a
specification into code is called "design" and that process is
creative.  You can't (yet? :-) automate creativity.  However, there
are things like refinement calculi that make the formal design process
`easier'...

You can try to write your design in an "executable subset" of a
specification language, but then you're throwing away a lot of the
expressiveness that the mathematics gives you anyway...

    Simon> [...]

    Simon> My suspicion is that no matter what kind of tools or
    Simon> languages or whatever you might try to apply to the
    Simon> problem, there's just no way to turn a complex task into a
    Simon> simple task, or even to reduce the complexity by anything
    Simon> approaching an order of magnitude. So it'll never be
    Simon> noticably easier to make provably correct software systems
    Simon> . . . The real gains would likely lie in coming up with
    Simon> processes that made it practical to approach that level,
    Simon> without being prohibitively expensive.

You've pointed out a large part of the problem here: complexity.
Software is very complex.  The decomposition is hard.  Most people
can't keep a very large problem in their head - think of the people
who are really good at software and you'll probably realise they're in
the minority who can, and many of them are OSS maintainers for big
projects.  :-)

We have the "programming in the small" thing nailed, and have had for
years, but only for the easily `abstractable' parts of applications.
This is why there is no excuse for (re)writing a broken version of one
of the algorithms or data structures that appear in undergraduate
textbooks.  All of these reusable things are solved and their
implementations can be proved correct.  What's more, if you use nice,
high-level (academic, generally poor-performing) languages, the proofs
get a lot easier.  One problem is that lots of "coders" can't cope
with the required mathematics or the abstraction in the neat
programming languages.

Some things are harder:

* decomposing large systems; and

* talking to complex hardware (without a nice abstraction layer on top
  of it - yes, I know we're always talking to complex hardware, but
  usually we don't have to know about it).

The really hard thing is managing complexity.  Most people are simply
not good at it, and most of those are "professional software
engineers".

One way of managing complexity is to build a model of a system that is
abstract enough so that it hides enough complexity so that you can
cope.  You can then reintroduce the complexity when you specify the
internals of the relevant pieces.  Again, abstraction is hard...

    Simon> Anyone who can prove me wrong will be worshipped,
    Simon> deservedly ;-)

I don't think I've proved you wrong, but feel free anyway...  :-)

peace & happiness,
martin