From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id GAA08459; Sun, 11 Nov 2001 06:24:42 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id GAA07865 for ; Sun, 11 Nov 2001 06:24:41 +0100 (MET) Received: from gogol.zorgol (Mix-Montsouris-109-1-210.abo.wanadoo.fr [193.248.100.210]) by concorde.inria.fr (8.11.1/8.10.0) with SMTP id fAB5Ocn20227 for ; Sun, 11 Nov 2001 06:24:39 +0100 (MET) Received: (qmail 16162 invoked by uid 1001); 11 Nov 2001 05:17:46 -0000 Date: Sun, 11 Nov 2001 06:17:46 +0100 From: Berke Durak To: caml-list@inria.fr Subject: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease Message-ID: <20011111061746.A214@gogol.zorgol> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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