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

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

[Berke Durak]

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

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

[Eric Newhuis]

<seriousness>
Is there a market for such a thing?  Defense?  Secure operating systems?
What are all the tangible benefits?
</seriousness>

<humor>
What will the name fo the OS be?  SafeLix?  FreeBSafeD?
</humor>

<opinion>
Windows NT might already be part of the way there depending on how one views
Prolog as being closer to Caml.  I guess they're both functional.  Has
Prolog, used in the following manner, added the safety you hope to achieve?
And could Caml have also achieved it?
</opinion>

<fact>
Microsoft used Prolog in NT's network stack.
http://research.microsoft.com/research/dtg/davidhov/pap.htm
</fact>

-------------------
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

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

[Tom]

There are is probably a lot more non-C/C++, safe software in Linux and
UNIX than in Windows NT.  Linux and UNIX use shell, Perl, Python, and
awk extensively--safe, high-level programming languages (if dynamically
typed).  Linux installations often also use cfengine, a kind of expert 
system shell for system configuration.  And this is nothing new: 15 years
ago, statistics at Bell Labs showed that people spent a lot more compute
cycles in awk than in native C programs.

Still, dynamic languages have their limitations, and it would be 
nice to rethink and build larger parts of the Linux
environment in ML, in part to achieve more safety, and in part to make
it easier to modify and extend system software.  Both UNIX and ML 
would benefit from the experience and results.  Utilities 
like "unison" and "bibtex2html" (both written in OCAML)
are a good indication that ML can be used for such applications.

I think most people don't spend much time on it because there isn't
really a big itch that needs to be scratched for them.  Apache, or "GNU 
ls", may both be messy, hard-to-maintain C programs, but they get the
job done and someone else is doing the testing, so why bother 
rewriting them?  Still, all it takes is volunteers, so go ahead 
and pick a project.

Tom

--- Eric Newhuis <enew@bigfoot.com> wrote:
> <seriousness>
> Is there a market for such a thing?  Defense?  Secure operating systems?
> What are all the tangible benefits?
> </seriousness>
> 
> <humor>
> What will the name fo the OS be?  SafeLix?  FreeBSafeD?
> </humor>
> 
> <opinion>
> Windows NT might already be part of the way there depending on how one views
> Prolog as being closer to Caml.  I guess they're both functional.  Has
> Prolog, used in the following manner, added the safety you hope to achieve?
> And could Caml have also achieved it?
> </opinion>
> 
> <fact>
> Microsoft used Prolog in NT's network stack.
> http://research.microsoft.com/research/dtg/davidhov/pap.htm
> </fact>
> 
> -------------------
> 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


__________________________________________________
Do You Yahoo!?
Find a job, post your resume.
http://careers.yahoo.com
-------------------
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

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

[Sven]

On Sun, Nov 11, 2001 at 06:17:46AM +0100, Berke Durak wrote:
> 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.

...

A most interresting project, i would be higly interrested by it.

My previous thinkings about it would have me worried about the low level
access stuff.

How does ocaml and its garbage collection interract with things like handling
non-cacheable driver IO memory, or maybe the DMA-able pages sent to your SCSI
driver or graphic card ?

A worthy project, but i assume somewhat really big (after all, linux represent
10 years of developpment by thousands of very competent programmers all over
the world). A more realistic thing would be a small ocaml written kernel for a
small embedded system, with a limited set of peripherics. Once that is done,
you can go ahead and propose a more complete system.

Friendly,

Sven Luther
-------------------
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

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

[Julian Assange]

> well-accepted brand of UNIX should be reimplemented in that language.

Re-implementation is a great option for people whose creative wik
flickers, who suffer the belief that the best one can hope for
is a 10% improvement in already imbodied ideas.

But the program yet to be written, whose form remains unknown to
silicon and people alike, has an infinity of improvement ahead of it.

--
 Julian Assange        |If you want to build a ship, don't drum up people
                       |together to collect wood or assign them tasks and
 proff@iq.org          |work, but rather teach them to long for the endless
 proff@gnu.ai.mit.edu  |immensity of the sea. -- Antoine de Saint Exupery
-------------------
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

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

[Jeff Henrikson]

> An appropriate sublanguage of Caml should be isolated, and a given,
> well-accepted brand of UNIX should be reimplemented in that language.

Well, I've heard lots of versions of comment before, and let's just say I'm not holding my breath for an industrial strength
solution.  Here's some prior art.  Olin Shivers at the MIT AI lab wrote an OS based on SML/NJ called ML/OS and called it "the
express project":

http://www.ai.mit.edu/projects/express/

More significantly, the toolkit he used seems to be taking off a lot better. The Flux OS Kit from the University of Utah has about
10 client research projects.  The basic philosophy is that the "hello world" OS should be as easy to write as the "hello world" C
program.  They have cannibalized a lot of functionality from Linux and FreeBSD, including various device driver models.

http://www.cs.utah.edu/flux/oskit/projects.html

And then, for the ultra-hyper-purist who takes purity above progress at all cost, there's Tunes, which has looked about as
undeveloped as it does now for the last seven years.  The idea here is an os which can be quieried, "Print me out a copy of your
own source code decompiled.  Then instrument in ways x, y and z, compile it, and dynamically load the changes back into yourself."
They plan on doing this with a untyped low level language which is like a compiler intermediary form for a GCed language, plus a
high level language which is like scheme with a type-and-various-other-properties proof system added on.

http://tunes.org/

When will tunes be ready?  Well, my first comment was not my own.  In their own words, "Don't hold your breath (tm)."


Jeff Henrikson

-------------------
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

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

[Mark Seaborn]

Berke Durak <berke@altern.org> writes:

[...]
> 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.
[...]

You may be interested in a project I am implementing at the moment:
The idea is to automatically translate any C program into a
memory-safe language.  This can be done by assuming that a block of
memory should only be accessed through values that depend on the
block's address.  The blocks that a value is dependent on can be
tracked at run time, but static analysis can be used to eliminate this
cost hopefully in most cases.  This scheme can be applied to turn
filenames, as well as pointers, into unforgable capabilities.

I've written a draft paper explaining this which is at:
<http://www.srcf.ucam.org/~mrs35/comp/safe-c/making-c-programs-safe.txt>

-- 
         Mark Seaborn
   - mseaborn@bigfoot.com - http://www.srcf.ucam.org/~mrs35/ -

  ``Every revolutionary opinion draws part of its strength from a secret 
      conviction that nothing can be changed'' -- George Orwell
-------------------
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

[Caml-list] GCCXML: don't write your own C parser. (WAS: Rewriting UNIX . . .)

[Jeff Henrikson]

> You may be interested in a project I am implementing at the moment:
> The idea is to automatically translate any C program into a
> memory-safe language. . .

You're obviously going to need a parser and I presume you don't want to write one.  Make sure to check out this extenion to GCC
which prints out an XML abstract syntax tree of anything GCC can parse.

http://public.kitware.com/GCC_XML/

Note that this is not _real_ XML, as there is no DTD.  But the file xml.c could be easily hand translated into a recursive set of
variants that would be about 150 lines of caml, along with a simple stream parser could do the task of building the tree.  I'm
going to write such a thing Real Soon Now, as I think it would be especally interestng to do other sorts of C/C++ metalingustic
hacking on account of the vast amount of available code.  (But if you really need it, don't wait for me, as I get busy often)

If anybody reads the GCCXML link and thinks of the most obvious application of stub-code generators for FFI mucking, that's both
why it was written and why I'm playing with GCCXML.  CamlIDL requires too much manual effort; I think the best evidence is
hearing/seeing so many hand written wrappers.  I see no reason for directly handling the raw C code.  I want something like the
SWIG typemap model but cleaner, with an emphasis on not having to edit the original header files.  I went so far as to mostly
implementing a SWIG 1.3.7 module for ocaml, so I see it's strengths and weaknesses.  But SWIG is not probably going to be a correct
or clean program any time soon, so I'd like to clean it up and add some power.  If anybody wants more info I can prodded to write
it down for you.


Jeff Henrikson



-------------------
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

Re: [Caml-list] GCCXML: don't write your own C parser. (WAS: Rewriting UNIX . . .)

[Berke Durak]

On Mon, Nov 12, 2001 at 12:33:47PM -0500, Jeff Henrikson wrote:
> > You may be interested in a project I am implementing at the moment:
> > The idea is to automatically translate any C program into a
> > memory-safe language. . .

Sounds particularly interesting.

> You're obviously going to need a parser and I presume you don't want
> to write one.  Make sure to check out this extenion to GCC which
> prints out an XML abstract syntax tree of anything GCC can parse.

> 
> http://public.kitware.com/GCC_XML/
> 

Very good idea. Indeed I got that idea about rewriting UNIX in Caml last
day when I was trying to Camlify a YACC grammar for ANSI C. And most
programs are far from being ANSI C (everyone has certainly used GNU
extensions ?). So, since we're fighting against C, and since GNU C is
the most widespread GNU compiler, directly using GNU C's output
seems to be the most useful approach. Since Caml is dependent on C,
it would be fair enough to be able to easily manipulate C programs
in Caml.

> I'm going to write such a thing Real Soon Now, as I think it would
> be especally interestng to do other sorts of C/C++ metalingustic
> hacking on account of the vast amount of available code.  (But if
> you really need it, don't wait for me, as I get busy often)

A well-designed C syntax module, both parsing and unparsing, would be really
great. It would be very useful for :

1) Emitting C code (could be applied to FFTW or CamlIDL)
2) Creating automatic code obfuscators
3) Playing with C semantics (experiments in model-checking etc.)

A C ``interpreter'' could be thus written. I've already seen a Java course
taught using Caml. It could be useful for teaching (eg. ``Exercice. Write
a Caml program that removes for-loops from C programs'')...
--
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

Re: [Caml-list] GCCXML: don't write your own C parser. (WAS: Rewriting UNIX . . .)

[Julian Assange]

> A well-designed C syntax module, both parsing and unparsing, would be really
> great. It would be very useful for :
> 
> 1) Emitting C code (could be applied to FFTW or CamlIDL)

Or, bigloo like, parsing C .h files for transparent foreign function support.

--
 Julian Assange        |If you want to build a ship, don't drum up people
                       |together to collect wood or assign them tasks and
 proff@iq.org          |work, but rather teach them to long for the endless
 proff@gnu.ai.mit.edu  |immensity of the sea. -- Antoine de Saint Exupery
-------------------
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