Re: HURDNG : Which type of OS design could we have to think nowadays ?

[Jonathan S. Shapiro]

On Mon, 2006-08-07 at 22:36 +0200, Guillaume FORTAINE wrote:
> I believe that my underlying hope is to see joined together the best men 
> with a strong background to produce the best "theory" : the "ultimate 
> convergence" ( like SoC, quadruple play, ...) => create the 
> state-of-the-art to see more higher ...

Hmm. I am not sure that I am understanding your conjunctions correctly,
so what I am about to say may not be necessary.


I am deeply uninterested in producing the best theory. Perhaps it would
be better to say: different people have different ideas of "best", and
people who do theory professionally usually have a view that is very
different from mine. So what I mean is: I am not interested in producing
the best theory **qua theory**.

The reason that I am excited about the BitC project is that I think we
may be able to bridge a gap here between theory and practice in a way
that will have significant benefit for the practice of critical software
construction. What interests me is theory that is applied for some
practical purpose, and more specifically theory that is applied to the
practical problems that I am trying to solve.

In my heart, I am an engineer, not a scientist, and not a theorist. I am
certain that we will need to expand the body of theory about programs,
types, and provers in order to do any useful verification in BitC, and I
think that will be fun. I am not interested in expanding the theory for
its own sake.

I greatly enjoy working with theory people. This is not an "us vs. them"
type of statement. Rather, it is a statement about where *I* stand. I
view myself, in this context, as a bridge builder and (hopefully) an
integrator of ideas.



shap