[Yhc] Verified compiler
guillaume.fortaine at wanadoo.fr
Fri Aug 25 22:22:04 EDT 2006
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
More information about the Yhc