[Caml-list] Rewriting UNIX in Caml and getting rid of the C disease

[Berke Durak <berke@altern.org>]

Everyone on this list will agree that the C language is far from being
perfect. More specifically, if we consider its various derivatives
together (i.e. the C preprocessor and C++) they form the worst piece
of stinking, pathogen and toxic garbage in the realm of programming
languages.

On the other hand, we almost all use and respect UNIX and its
derivatives, which might seem to be a paradox, given that UNIX is
entirely based on C.  I'm here considering UNIX from the system
programmer's view, making abstraction of the way it's
implemented. Certainly, it could get much better, but, practically, it
is just fine.

Unfortunately, the C language acts as a mandatory layer over
UNIX. Generating an executable for a given brand of UNIX without going
thru the C library is tricky because it requires to know how the
system calls work. These are, first, not documented (because you're
supposed to go thru the C library), and, second, depend precisely on
#ifdef-infested C source code, and are subject to revision.

Therefore, in the interests of humanity, I hereby propose that :

                              ***

An appropriate sublanguage of Caml should be isolated, and a given,
well-accepted brand of UNIX should be reimplemented in that language.
Binary compatibility must be retained as far as possible. Basic system
utilities (including a shell) should also be translated (into full
Ocaml). Since the use of Caml will, a) divide the source code size by,
say, ten and b) automatically remove, say, 95% of all bugs and
security holes (since most are illnesses resulting from pointer
manipulation), success is guaranteed.

                              ***

Progress has to be made in operating systems. C blocks that progress.
C must be obliterated.

The use and existence of a Caml-based UNIX, with a (justified)
reputation of very good security and integrity, will invariably
attract a lot of hackers (in the good sense) to Caml. It will also
make existing Caml programmers a valuable resource.

The use of Caml might also facilitate the verification of some parts
of it using Coq, even if I don't know what part of an operating system
you could usefully verify by formal methods.

For marketing purposes, a bijective mapping between some sort of
subgrammar of C and the sublanguage of Caml could be provided.

For people worrying about speed, I'd just remind them that not so long
ago, C itself was considered pretty slow and inefficient a language
(maybe the compilers weren't as good), yet operating systems 
were written in C and used on computers a thousand times slower than
what we have today.

Finally, the task of translating UNIX from C to Caml, if certainly
not straightforward, is certainly feasible with a predictable amount
of work, and could even be made semi-automatically.
--
Berke
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr