Re: Formal methods?

[Mark Seaborn]

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.
Functional languages are often regarded as `executable
specifications'.  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.

-- 
         Mark Seaborn
   - mseaborn@bigfoot.com - http://members.xoom.com/mseaborn/ -

                  How to write good:
          ``7. It is wrong to ever split an infinitive.''