Re: Interested in Formal Methods

[Patrick Strasser]

a hafiz wrote:
> i share your interest in Formal Methods and especially in applying it to
> HURD.  I have heard of VDM and B but not actually read about them let
> alone use them. But i did do  some Z while in Uni. and although it was
> difficult at first but once you get it, it's not too bad and i started
> to like it! i thought Z was fun! (maybe something wrong with me...)

We work with NewJersey-SML and we expand it to SadoMasoLanguage, and...
half a year later... I like it. I think this first antipathy comes from
the fact that nearly everyone learning a fromal language has used
imperative languages like C before. You have to change your way of
"thinking" code.

> Jason More, had a valid point about the whole thing. Formal Method can be
> very hard, and the amount of effort expended to apply it to HURD may not
> be worth the small gain. it might still be interesting and fun though!
> so IF i were to do it, it would be just for the heck of it and hopefully
> there would be some sort of academic value to it, so it won't be a complete
> waste. I have actually toyed with the idea myself but not knowing much about
> Zed or OS design, it just remains an interest for me.

How can you tell? The Hurd gives us the oportunity to change a small
part of the system and test it in "real life" in a working context. Work
has to start in small steps. What could be a starting point? Some
translator? Some additional frome the Task list (ps)?
Second, a foraml language is more secure due to more abstraction.
 
> finally, my personal opinion on formal methods is that, it is not so
> much the method or notation, but it is what the method or notation forces
> you to do. What formal methods does is force you to think about your design
> a bit more thoroughly and it guides you to do it correctly. when you just
> draw some design base on some simple specs you tend to just do a quick
> sketch and straight away jump to the coding. with formal methods, you are
> more likely to expand your original idea, and explore the problem a little
> more.

I.e. work is the same, but with formal languages you don't need to hunt
bugs for nights...

Patrick