From: Mark Seaborn <[EMAIL PROTECTED]>
Subject: Re: Formal methods?
Date: 04 Dec 2000 17:50:39 +0000
> Atle <[EMAIL PROTECTED]> writes:
>
> > 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 <[EMAIL PROTECTED]> who will specify Linux in Z or
> > B, and with some help I might have a go at a Hurd subsystem.
>
> 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.
I agree that this would be interesting...
> Functional languages are often regarded as `executable
> specifications'.
IMHO this statement is too bold. Consider the specification taken from
the "Larch: Languages and Tools for Formal Specification"
int sqrt(int x) {
requires x \ge 0;
modifies nothing;
ensures \forall i : int
(abs (x - (result*result)) \le abs(x - (i*i)));
}
this specification will allow many implementations. Nonetheless,
functional languages are *much closer* to formal specification and due
to formal semantics for the language as well as properties such as
referential transparency are much easier to formally reason about than
say C.
> Proving a large C program correct is difficult and
> does not give you much at the end of the day, whereas an
> implementation in a functional language will be easier to inspect for
> correctness and easier to modify in the future.
Marko
_______________________________________________
Help-hurd mailing list
[EMAIL PROTECTED]
http://mail.gnu.org/mailman/listinfo/help-hurd
