On Tue, Sep 15, 2009 at 9:00 AM, William Leslie < [email protected]> 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
