Re: Formal methods?

[Marko Schuetz]

From: Mark Seaborn <mrs35@cam.ac.uk>
Subject: Re: Formal methods?
Date: 04 Dec 2000 17:50:39 +0000

> Atle <trollet@skynet.be> 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 <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.
> 
> 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