Re: is Linux obsolete?

David Monniaux (monniaux@clipper.ens.fr)
Tue, 8 Jun 1999 21:21:58 +0200 (MET DST)


AmigaDOS, or at least its early incarnations that ran on A500, A1000's,
didn't implement memory protection. This of course reduces overhead
considerably when it comes to layer separations. No expensive copies; no
context switching...

I have not yet heard of any efficient way to handle memory protection
between layers. If somebody is aware of something neat in this area,
please let me know.

As for kernel safety through type safety: indeed type safety as in
traditional languages can catch lots of errors - my experience is that
developing in Caml (http://caml.inria.fr) is much more pleasant than in
C, especially when it comes to bugs. However, usually stronger invariants
than mere elementary type safety are required; a ML-like type system
can't encompass notions like "a and b are lists and the sum of their
lengths is the product of c and d". You can do that using more elaborate
type systems (see Coq, http://coq.inria.fr); this amounts to providing a
proof of safety with the code (see the works on proof-carrying code, for
instance George Necula's). This is still highly experimental, since the
programming hassles and the experience required for such safe programming
exceed what is bearable by the general industry (the situation is
different for critical embedded systems).

This is beginning to be quite out-of-topic for the Linux-kernel list,
since it's more of a general discussion on OS and language designs...

-- David

-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/