Formal methods?

[Atle]

Hello!
Keeping quiet for a while, I feel it is time to ask (again?):
What is the general attitude toward using formal methods (VDM-SL, Z, ...) in 
the development of parts of the system?
I guess you are all aware that in 20 years, no software will be built without 
formal methods, just like nobody uses a hammer and saw
(or whatever Henry Ford used :) to build a car anymore.
Cars, planes, bridges, spacecraft, houses - everything is subject to rules of 
engineering.
Only software construction has until now 'escaped' - because it is a new 
engineering discipline
(programming is *NOT* an artform! :-)

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.

But I will need help from someone who really knows the module, prefereably the 
author or maintainer.
And nothing will be 'obvious' or 'self-explanatory' - everything has to be 
specified down to the most 'insignificant' detail, with
domain specification, codomain (range), pre-conditions, post-conditions, 
invariants for data and loops, reification from a high
level of abstraction down to bit-level ... a BIG, BIG job!!!

Anyone interested?

Atle