Re: Formal methods?

[Jason S. Moore]

Well, this is a little off subject but oh well :)

There are people that have been preaching about formal methods for 20 years
already and it just hasn't happened. Isn't it a bit presumptious to say that it
will only take another 20 years for people to see the 'light'. 

Also comparing software engineering to other forms of engineering is like
comparing apples and oranges. Some forms of civil or mechanical engineering have
been around for over a millenium. Those diciplines have had a much longer time
to perfect their methods and it's absurd to think that software engineering can
catch up in the 80 years that people have been developing software. Those
diciplines also have physics as a final set of rules that they have to follow,
and while physics has changed as far as our understanding of it, it's the same
it was a long long time ago. Programming in general doesn't have an underlying
set of rules like physics that it has to follow.

As far as formal methods go, I think they all are too much work for too little
gain. If someone has to specify everything, then they are practically writing
the program already, so I belive that the time is better spent on the actual
programming. I'm not saying that spending time designing a system or component 
is a waste, just that the detail required by most formal specification is just
wasted time. If there is a clear overall design, then I think it's better to let
the, hopefully not incompetent, programmers deal with the details.

Well there's my rant for the day. :)


On Fri, 01 Dec 2000 18:35:16 +0100
Atle <trollet@skynet.be> wrote:

> Hello!
> Keeping quiet for a while, I feel it is time to ask (again?):
> What is the general attitude toward using formal methods (VDM-SL, Z, ...) in 
> the development of parts of the system?
> I guess you are all aware that in 20 years, no software will be built without 
> formal methods, just like nobody uses a hammer and saw
> (or whatever Henry Ford used :) to build a car anymore.
> Cars, planes, bridges, spacecraft, houses - everything is subject to rules of 
> engineering.
> Only software construction has until now 'escaped' - because it is a new 
> engineering discipline
> (programming is *NOT* an artform! :-)
> 
> In February I will take a course about large projects, with an OS as a case 
> study.
> There is one guy, teacher of formal methods, Georges Mariano 
> <georges.mariano@inrets.fr> who will specify Linux in Z or B, and with
> some help I might have a go at a Hurd subsystem.
> 
> But I will need help from someone who really knows the module, prefereably 
> the author or maintainer.
> And nothing will be 'obvious' or 'self-explanatory' - everything has to be 
> specified down to the most 'insignificant' detail, with
> domain specification, codomain (range), pre-conditions, post-conditions, 
> invariants for data and loops, reification from a high
> level of abstraction down to bit-level ... a BIG, BIG job!!!
> 
> Anyone interested?
> 
> Atle
> 
> 
> _______________________________________________
> Help-hurd mailing list
> Help-hurd@gnu.org
> http://mail.gnu.org/mailman/listinfo/help-hurd


--
Jason S. Moore, King of the Slackers
Student, University of Colorado at Colorado Springs
GPG KeyID: 1A5B24AA                             Keyserver: 
http://pgp5.ai.mit.edu/