[Sussex] Microsoft fails to comply

[Steve Dobson]

Hi Mark

On Sat, Mar 19, 2005 at 11:47:36AM +0000, Mark Harrison (Groups) wrote:
> Steve Dobson wrote:
> 
> >4). The F/OSS movement, despite (or maybe I should say "because of") it
> >   having no leader, is now the most powerful software process on 
> >   the planet.  It has been proved that it can produced code which is
> >   much more stable, bug free, and well designed code.  It betters 
> >   all formal design methods!!!
> > 
> >
> Most, not all.
> 
> The one formal design method that can be clearly demonstrated to be 
> better was the one that INMOS used for the transputer and OCCAM.
> 
> This used a technique of formal mathematical modelling, denotational 
> semantics, and proof theory to build a chip (the T8000 transputer) that 
> could be properly demonstrated to be completely bug-free. (It is my 
> understanding that, after 15 years, this is still held to be true and 
> no-one has found a bug in the T8000 nor in its Occam compiler.)

I did formal mathematical methods when I was at Poly.
 
> The downside of this was that, on inspection, there only approved to be 
> about a dozen people in the world who actually understood formal proof 
> of parallel algorithms well enough to put this methodology into 
> practice. Even some of the key textbooks turned out to have errors in 
> them in the more esoteric bits :-) As a result of this, the development 
> programme was stopped in the early 90s.
 
The one think that I do remember from my mathematical is that working out
the pre- and post-conditions were the hardest part.  For algorithms it is
easy, like sorting:

     Given an array A of size n
     for each i (0 < i < n - 2) A[i] <= A[i+1]

But what is the post condition for a Word document?  Or this e-mail?
Not all applications lend themselves to a method which is why I 
discount formal methods as a failed method along with JSP, OO, UML, ...

> I agree, absolutely, however, that F/OSS is now the most powerful 
> software process on the planet. And that it has been clearly 
> demonstrated that it can produce code that is stable, bug free and 
> well-designed, and that it betters any formal design method that has 
> been used by any successful proprietary vendor.

F/OSS works (IMHO) not because it abandons the other methods but because
it abandons the need to use just one.  All formal methods that I have 
ever been taught try to remove the random element from the design process.
Why?

If you can test every product to check that it is up to par, then random
sampling is the best way of testing.  Randomness is built in the the very
rules that govern the way the universe works: we have quantum mechanics,
and natural selection (to name but two).

Why, oh why, then do we not embrace randomness in more aspects of our
daily lives?

Steve