On software quality and engineering

[Simon Fowler]

On Sun, Nov 03, 2002 at 01:14:50AM +1100, David Gibson wrote:
> On Sat, Nov 02, 2002 at 04:18:30AM +1100, Michael Bennett wrote:
> [snip]
> 
> > Software systems do exactly what you tell them to do. The problem is most 
> > people don't know what they want the software to do and just guess. Which 
> > comes down to requirements and specifications. There are formal specification 
> > languages that can be used to mathmatically prove the specification. Most 
> > people don't use them as it takes too much time and more effort when they 
> > could be programming. I know some companies now use them for all software 
> > projects as they can produce software with zero defects.
> 
> More to the point, once you put the specifications into a formal
> language, it's not clear that it's significantly easier to tell that
> the specifications are correct than to tell that the code is correct.
> 
Another point is that if you have the specification in that formal
language, then you effectively /have/ the code - if the formal
language is sufficient to describe the system completely, then it
should be equivalent to the code for the system. Equivalent meaning
automatically translatable to the code (and hence to the final
executable). 

I think that's where the ML family of languages actually started
out: as part of a formal program proof system (ML meaning "Meta
Language", incidentally). 

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

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

Simon

-- 
PGP public key Id 0x144A991C, or http://himi.org/stuff/himi.asc
(crappy) Homepage: http://himi.org
doe #237 (see http://www.lemuria.org/DeCSS) 
My DeCSS mirror: ftp://himi.org/pub/mirrors/css/ 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 232 bytes
Desc: not available
Url : http://lists.samba.org/archive/linux/attachments/20021103/9aec3033/attachment.bin