Hello Misters, As you are compiler experts, I am asking your help. I am attempting to build up a team. I believe it's time for a full-fledge verified OS. If somebody is interested in functional programming and in formal methods to help to implement a verified compiler , he is welcome :) Here are two examples of a compiler formalisation : http://pauillac.inria.fr/~xleroy/compcert-backend/ http://www.score.is.tsukuba.ac.jp/~okuma/vc/ Another intereesting link : http://pes.cs.tu-berlin.de/cocv2007/ And finally the ultimate goal : http://www.cse.ogi.edu/~hallgren/House/ http://web.cecs.pdx.edu/~rebekah/presentations/ssp2005abs.pdf http://web.cecs.pdx.edu/~rebekah/papers/icfp05_bits.pdf Haskell also depends on a complicated run-time system. Such run-time systems are often unverified. Implementing a minimal, high-assurancerun-time system is a topic for future work. http://www.oreilly.com/catalog/opensources/book/linus.html GCC Unix itself is a great success story in terms of portability. The Unix kernel, like many kernels, counts on the existence of C to give it the majority of the portability it needs. Likewise for Linux. For Unix the wide availability of C compilers on many architectures made it possible to port Unix to those architectures. So Unix underscores how important compilers are. The importance of compilers was one reason I chose to license Linux under the GNU Public License (GPL). The GPL was the license for the GCC compiler. I think that all the other projects from the GNU group are for Linux insignificant in comparison. GCC is the only one that I really care about. A number of them I hate with a passion; the Emacs editor is horrible, for example. While Linux is larger than Emacs, at least Linux has the excuse that it needs to be. But basically compilers are really a fundamental need. Now that the Linux kernel follows a generally portable design, at least for reasonably sane architectures, portability should be possible as long as a reasonably good compiler is available. For the upcoming chips I don't worry much about architectural portability when it comes to the kernel anymore; I worry about the compilers. Intel's 64-bit chip, the Merced, is an obvious example, because Merced is very different for a compiler. So the portability of Linux is very much tied to the fact that GCC is ported to major chip architectures. If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr I will set up a mailing-list, a web server, a wiki and an IRC Best Regards, Guillaume FORTAINE