caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
@ 2001-11-12 21:52 Arturo Borquez
  0 siblings, 0 replies; 10+ messages in thread
From: Arturo Borquez @ 2001-11-12 21:52 UTC (permalink / raw)
  To: berke; +Cc: caml-list

On Sat, 10 November 2001, 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.
> 
> 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.
> 

I agree with you that C/C++ are the most pathological
and toxic programming languages ever made, but at UNIX
OS kernel level they do quite well (because the huge
amount of manpower invested in debugging by miriads of 
programmers and testers thru last 10 years). and are
fairly stable and reliable. I am not sure that the
effort porting actual C based kernel would be 'payed'
to achieve substantial results. What is really wrong is
using C in high level apps. I think that is better to
build a parallel version of Caml libraries to interact
directly with the kernel thru a Caml System Abstraction
Layer (CSAL), bypassing intermediate messy, fragmented,
specifical to C limitations libraries. Then at a second
stage when CSAL implemented and working, perhaps it
will be the time to replace the whole  C kernel. The
benefits of this aproach are:

1)legacy UNIX software will work seamlessy with the
traditional lib's support, or it would be necessary to
provide API compatibility to it.

2)CSAL will be designed to take full advantage of Caml
language (or not necessary to built it arround actual
lib design?). Full multithreading and dynamic linking 
should be provided to work properly with CSAL, an some
GC adaptations?.

3)Legacy Caml apps will also work seamlessy as pointed
in 1) with traditional libs. Moreover it will allow to
do 'mixed' apps.

4)GC timing overhead will be mitigated thru a more
'direct' acces to system resources (More than 90%+ of
time programs are excuting inside lib's code)
shortening the path to 'active code' and reducing the
number of calls needed to complete a usefull action. 

5) It seems me this strategy is not as radical as you
propose and don't put aside the idea of a 'total'
replacement, but doing it in two steps so with limited
Caml manpower would be more doable?. It also allow an
'incremental' developemt of CSAL with Caml, deprecating
old environment gradually as CSAL evolves. 

My proposal is a 3 layer model,

native-unix-kernel->CSAL->Caml apps.

to reach the final model,

caml-unix-kernel->CSAL->Caml apps.

Another important issue is that this SAL should be
be compliant with POSIXS or not?, or if we should have
full freedom to define it at the best to fit with Caml
features and more 'modern' design?.
My opinion favours the later, in spite it would take an
aditional step defining what's the 'modern' design is.
The pricipal drawback of this proposal is this CSAL
will be CAML propietary, as no third party languages
API's will be provided, nor it will intedended to do.
It will need maintaining support as UNIX kernel's
evolves. This fact will also constrain CSAL to kernel 
limitations.

I think that a project like this would need the
aproval, support and commitment of INRIA, and I don't know if this idea is barely considered in their plans,
prorities? (it seems me not).

Undoubtly OS design and languages, have a great 
importance and makes a big difference (productive
time /(productive time + wasted time)), on all stuffs
derived from them. It is unbeliable the ignorance and
misunderstanding I've found among industry IT's and
'engineers' who are still using CRAPS.   

Best Regards
Arturo


Find the best deals on the web at AltaVista Shopping!
http://www.shopping.altavista.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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  2001-11-21 21:25 Michael Hicks
@ 2001-11-22  3:10 ` Rafael 'Dido' Sevilla
  0 siblings, 0 replies; 10+ messages in thread
From: Rafael 'Dido' Sevilla @ 2001-11-22  3:10 UTC (permalink / raw)
  To: Michael Hicks


On Wed, Nov 21, 2001 at 04:25:12PM -0500, Michael Hicks wrote:
> 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

Oh, a GC is not required?  Last time I checked the website it used the
Boehm-Demers-Weiser conservative garbage collector.  So the only time a
GC is not required is when your program does little or NO heap
allocation whatsoever...  The FAQ says:

Q: Can I call free?
A: No, individual memory objects may not be freed. In future versions,
we may support freeing objects for which you can prove that there are no
other pointers to the object. Until then, you must rely on a garbage
collector to reclaim heap objects or use regions (similar to ``arenas''
or ``zones'') for managing collections of objects.

Thus Cyclone doesn't (yet anyway), give the programmer that much control
over memory management.  But hey, the compiler is still at Version 0.2
so it's got a long way to go...

> 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

This was one of the first things I noted about it, as these days I'm
just beginning to learn Caml myself and ran into Cyclone just a few days
ago (thanks to aleph1)...

Looks very cool.  Might be a better language to write a next-generation
OS in once it matures some more, but yes, for applications that don't
require intimate contact with the machine (almost all applications fit
into this category), Caml may work better.

-- 
Rafael R. Sevilla <sevillar@team.ph.inter.net>   +63(2)   8177746 ext. 8311
Programmer, Inter.Net Philippines                +63(917) 4458925
http://dido.engr.internet.org.ph/                OpenPGP Key ID: 0x5CDA17D8
            Heute die Welt und Morgen das Sonnensystem!
-------------------
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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* RE: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
@ 2001-11-21 21:25 Michael Hicks
  2001-11-22  3:10 ` Rafael 'Dido' Sevilla
  0 siblings, 1 reply; 10+ messages in thread
From: Michael Hicks @ 2001-11-21 21:25 UTC (permalink / raw)
  To: Berke Durak, caml-list

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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  2001-11-11  5:17 Berke Durak
                   ` (3 preceding siblings ...)
  2001-11-12  8:32 ` Jeff Henrikson
@ 2001-11-12 13:39 ` Mark Seaborn
  4 siblings, 0 replies; 10+ messages in thread
From: Mark Seaborn @ 2001-11-12 13:39 UTC (permalink / raw)
  To: caml-list

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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* RE: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  2001-11-11  5:17 Berke Durak
                   ` (2 preceding siblings ...)
  2001-11-11 13:32 ` Julian Assange
@ 2001-11-12  8:32 ` Jeff Henrikson
  2001-11-12 13:39 ` Mark Seaborn
  4 siblings, 0 replies; 10+ messages in thread
From: Jeff Henrikson @ 2001-11-12  8:32 UTC (permalink / raw)
  To: Berke Durak, caml-list

> 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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  2001-11-11  5:17 Berke Durak
  2001-11-11  6:11 ` Eric Newhuis
  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
  4 siblings, 0 replies; 10+ messages in thread
From: Julian Assange @ 2001-11-11 13:32 UTC (permalink / raw)
  To: Berke Durak; +Cc: caml-list

> 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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  2001-11-11  5:17 Berke Durak
  2001-11-11  6:11 ` Eric Newhuis
@ 2001-11-11 12:47 ` Sven
  2001-11-11 13:32 ` Julian Assange
                   ` (2 subsequent siblings)
  4 siblings, 0 replies; 10+ messages in thread
From: Sven @ 2001-11-11 12:47 UTC (permalink / raw)
  To: Berke Durak; +Cc: caml-list

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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  2001-11-11  6:11 ` Eric Newhuis
@ 2001-11-11  8:22   ` Tom
  0 siblings, 0 replies; 10+ messages in thread
From: Tom @ 2001-11-11  8:22 UTC (permalink / raw)
  To: Eric Newhuis, caml-list

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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
  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
                   ` (3 subsequent siblings)
  4 siblings, 1 reply; 10+ messages in thread
From: Eric Newhuis @ 2001-11-11  6:11 UTC (permalink / raw)
  To: caml-list

<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


^ permalink raw reply	[flat|nested] 10+ messages in thread

* [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease
@ 2001-11-11  5:17 Berke Durak
  2001-11-11  6:11 ` Eric Newhuis
                   ` (4 more replies)
  0 siblings, 5 replies; 10+ messages in thread
From: Berke Durak @ 2001-11-11  5:17 UTC (permalink / raw)
  To: caml-list

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


^ permalink raw reply	[flat|nested] 10+ messages in thread

end of thread, other threads:[~2001-11-22  3:12 UTC | newest]

Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2001-11-12 21:52 [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease Arturo Borquez
  -- strict thread matches above, loose matches on Subject: below --
2001-11-21 21:25 Michael Hicks
2001-11-22  3:10 ` Rafael 'Dido' Sevilla
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

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