[Yhc] Verified compiler

William DUCK guillaume.fortaine at wanadoo.fr
Fri Aug 25 22:22:04 EDT 2006

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 :



Another intereesting link :


And finally the ultimate goal :




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.


 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

More information about the Yhc mailing list