[ On Tuesday, August 19, 2003 at 06:38:01 (+0200), Matthias Buelow wrote: ]
> Subject: Re: gcc optimizer bug in netbsd-1-6 on alpha (gcc 2.95.3 20010315  (release) (NetBSD nb3))
>
> {\rant My wettest dreams are of a complete Unix-style system implemented 
> in ML, or a similar language.  Unfortunately, I guess, I will not see it 
> happen, at least not any time soon.

It's already been done once, in Concurrent Euclid, with the intention of
creating a "provably correct" implementation of a complete and useful
operating system -- but long ago when V7 was still "advanced".

	Concurrent Euclid, the Unix System, and Tunis
	by Holt, R.C.
	(Addison-Wesley, November 1, 1982)
	ISBN 0201106949

	http://plg.uwaterloo.ca/~holt/cv/books.html

Apparently there's a newer but less complete implementation in Turing
now too:

	http://www.holtsoft.com/books/minitunis.html

(though I don't think anything written in Turing can be considered to be
provably correct)

-- 
						Greg A. Woods

+1 416 218-0098                  VE3TCP            RoboHack <woods@robohack.ca>
Planix, Inc. <woods@planix.com>          Secrets of the Weird <woods@weird.com>