caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: "Michael Hicks" <mhicks@cs.cornell.edu>
To: "Berke Durak" <berke@altern.org>, <caml-list@inria.fr>
Subject: RE: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
Date: Wed, 21 Nov 2001 16:25:12 -0500	[thread overview]
Message-ID: <706871B20764CD449DB0E8E3D81C4D4301FA2278@opus.cs.cornell.edu> (raw)

Just to resurrect this thread:

Many of your observations on the inadequacies of C (and those of the
people who followed up) are addressed in a language being developed at
Cornell and AT&T Research called Cyclone.  It incorporates successful
high-level language features to ensure safety, but unlike most
high-level languages, gives the programmer control over data
representation and, to a large extent, memory management (e.g. a GC is
not required).  Furthermore, Cyclone is very close to C, thus
simplifying the process of porting legacy code (we actually parse a
superset of C, but our type-checker is more restrictive, as you would
imagine).  In essence, the language was designed with just your sort of
systems project in mind.  So far we have written a 40,000 line compiler
in Cyclone, and ported nearly 30,000 lines of systems code.

So that I'm not too off-topic, I should say that OCaml has been a strong
influence on Cyclone---many of the OCaml libraries and tools were ported
to Cyclone, and many of OCaml's features have been added to allow more
high-level programming, if desired, including exceptions, pattern
matching, tagged unions (i.e. datatypes), and others.  Of course,
"OCaml-like" is not OCaml itself; OCaml should be the language of choice
for applications where low-level control is not as important (of which
there are many).

http://www.cs.cornell.edu/projects/cyclone/ has more details.  There is
much
more to be done, and comments are welcomed.

Mike

> -----Original Message-----
> From: Berke Durak [mailto:berke@altern.org]
> Sent: Sunday, November 11, 2001 12:18 AM
> To: caml-list@inria.fr
> Subject: [Caml-list] Rewriting UNIX in Caml and getting rid of the C
> disease
> 
> 
> 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
-------------------
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


             reply	other threads:[~2001-11-21 21:25 UTC|newest]

Thread overview: 10+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2001-11-21 21:25 Michael Hicks [this message]
2001-11-22  3:10 ` Rafael 'Dido' Sevilla
  -- strict thread matches above, loose matches on Subject: below --
2001-11-12 21:52 Arturo Borquez
2001-11-11  5:17 Berke Durak
2001-11-11  6:11 ` Eric Newhuis
2001-11-11  8:22   ` Tom
2001-11-11 12:47 ` Sven
2001-11-11 13:32 ` Julian Assange
2001-11-12  8:32 ` Jeff Henrikson
2001-11-12 13:39 ` Mark Seaborn

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=706871B20764CD449DB0E8E3D81C4D4301FA2278@opus.cs.cornell.edu \
    --to=mhicks@cs.cornell.edu \
    --cc=berke@altern.org \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).