[Yhc] Verified compiler

[William DUCK]

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