On: Why Is C Faster Than Java (2009)

[bear8642]

Still approx. zero, but seL4 kernel's written in C and proven correct preventing many security holes memory control prevents

[erik_seaberg → bear8642]

Wasn’t that generated from Haskell source rather than handwritten, after years of formal verification of not only the source but also the C code generator and the final machine code?

[kobebrookskC3 → erik_seaberg]

afaik, the c is handwritten for performance reasons, and is manually proven to be a refinement of the executable haskell model. the haskell is then proven to be a refinement of an abstract, more succinct spec.

[nine_k → kobebrookskC3]

Fine! Now we have a way to write guaranteed safe C code.

It requires quite a lot of qualification from the development team, though.

[kobebrookskC3 → nine_k]

if ur fine with writing 4 lines of code a day from an expert...i guess

[nine_k → kobebrookskC3]

With endless bug-hunting in hastily-written C code, it could be fewer than 4 lines a day of completed code. (I hope nobody actually does so poorly, except while learning C.)

[kobebrookskC3 → nine_k]

of course, with unverified code, "completed" means absence of evidence of bugs, not evidence of absence.

[tsimionescu → bear8642]

seL4 is absolutely tiny, not a good example - it's probably smaller than log4j. Plus, it took years of PhD time to develop.

[iamtedd → bear8642]

seL4 was released as open-source in 2014. I know of the helicopter drone; have any other projects made use of seL4? If not, why not? My naive guess is that it's too hard to build on the project without introducing vulnerabilities and therefore negating the benefits of the kernel, but I'd love to be shown otherwise.