help-hurd
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Formal methods?


From: a hafiz
Subject: Re: Formal methods?
Date: Wed, 6 Dec 2000 17:15:06 -0800 (PST)

James, i agree with your point. But I also believe you could just mix
ASM, C, C++ and Haskell. If you have a good design with well defined
interfaces, you could code the highest level in Haskell, and where ever
performance is an issue rewrite those number crunching, processor intensive
stuffs with C or even ASM. As long as you maintain the interfaces.

Buy writing everything initially in Haskell, you could prove the interaction
of the subsystems and objects as well the functionality of the whole system
to be correct. This will result in a well defined interfaces. If the
runtime environment is not efficient enough, you just optimise where
ever necessary while maintaining the well defined interfaces

i guess this is like a prototyping style of development. an Exploratory
executable formal method as oppose to the purely abstract method of 
formal languages such as VDM and Zed.

of course this could all be just academic mumbo-jumbo pipe dream, because
in theory it sounds great. in practice? i think the prolem here
is that people lack the discipline , the patience and the
resources (ie money) to really spend the time to apply formal methods.

applying formal methods does cost a lot initially and this is usually the
reason people give up, after a long time of not seeing any direct concrete 
results they just dump everything and go back to traditional means. and
all that promise of greater savings later and lower total cost does not
seem all that desirable anymore.

hafiz.

--- JB <jamesb@northnet.com.au> wrote:
> Agree. Obviously boot code needs to be in ASM, but the applications
> components like servers and whatever could be in a language which the code
> is easier to manage, debug and prove its correctness. My votes are with
> Java
> and Standard C++. OOP the whole lot to the hilt.
> 
> James Buchanan
> 
> ----- Original Message -----
> From: "Chiaki Ishikawa" <Chiaki.Ishikawa@personal-media.co.jp>
> To: <mrs35@cam.ac.uk>
> Cc: <help-hurd@gnu.org>
> Sent: Wednesday, December 06, 2000 11:17 PM
> Subject: Re: Formal methods?
> 
> 
> > X-PMC-CI-e-mail-id: 14225
> >
> > Hi,
> >
> > >I think it would be much more useful and interesting to reimplement a
> > >Hurd server in a high level language, such as Erlang (which has a lot
> > >of support for concurrency) or a concurrent version of Haskell or ML.
> > >Functional languages are often regarded as `executable
> > >specifications'.
> >
> > How efficient the real-world implementation of the
> > language runtime of these languages such as Erlang, Haskell, or ML?
> >
> > Depending on the efficiency, I won't be surprised if some
> > application-oriented daemons are written in these
> > high-level languages: for example, some type of
> > encryption/certification servers may be written
> > for correctness with a small library
> > for number crunching.
> >
> > One of these days, proving the correctness and improving the
> > security of this type of servers
> > is very important.
> >
> > --
> >      Ishikawa, Chiaki        ishikawa@personal-media.co.jp.NoSpam  or
> >  (family name, given name) Chiaki.Ishikawa@personal-media.co.jp.NoSpam
> >     Personal Media Corp.      ** Remove .NoSpam at the end before use **
> >   Shinagawa, Tokyo, Japan 142-0051
> >
> >
> >
> > _______________________________________________
> > Help-hurd mailing list
> > Help-hurd@gnu.org
> > http://mail.gnu.org/mailman/listinfo/help-hurd
> >
> 
> 
> _______________________________________________
> Help-hurd mailing list
> Help-hurd@gnu.org
> http://mail.gnu.org/mailman/listinfo/help-hurd


__________________________________________________
Do You Yahoo!?
Yahoo! Shopping - Thousands of Stores. Millions of Products.
http://shopping.yahoo.com/



reply via email to

[Prev in Thread] Current Thread [Next in Thread]