On Tue, Sep 15, 2009 at 9:00 AM, William Leslie
<address@hidden> wrote:
The significance of BitC was that certain security properties could be proven
easier than using proof systems on top of C; a kernel, drivers, and
core servers that have the reliability and security features you are interested
in may be possible, but you are right that it would really be a rewrite.
Unfortunately, there are no great crowds of programmers ready to rewrite
the equivalent of a monolithic Unix kernel on demand.
I think this is not entirely accurate. In fact, we never got to the "proof" part of the project. The significance of BitC right now is that it is possible to write low-level systems code in a strongly typed, safe language with between 1% and 3% overhead relative to C. If you choose to use a strongly typed, safe language for this purpose, there is strong empirical evidence that you can eliminate about 50% of all bugs in the code immediately.
Shap has left behind a fairly complete specification for Coyotos - it's not
like the work the interested parties did over those seven (?) years just
disappeared. And you already have GNU :)
Shap also left behind a working implementation that actually runs on three architectures.
shap