3 ms·
I think the talk was titled as it was to emphasize that Rust here wasn't a tool that they chose to use to develop a robust OS, but a tool without which, develop
by adgjlsfhk1 5y ago
I think the talk was titled as it was to emphasize that Rust here wasn't a tool that they chose to use to develop a robust OS, but a tool without which, developing a robust OS is impossible. Without a language that enforces security (like C), it is demonstrably impossible to write a robust OS.
- ncmncm 5y agoL4 is coded in C. L4 is proven robust. QED: false.
- mkj 5y agoThe proven robustness isn't C, its Isabelle 92.9% Standard ML 3.0% Haskell 1.5% C 0.8% TeX 0.7% Python 0.5% Other 0.6% https://github.com/seL4/l4v https://github.com/seL4/l4v
- ncmncm 5y agoYou make no sense. The proof is obviously not coded in C because C is not a language you can write proofs in. But all of the instructions executed when running L4 were emitted by a C compiler. (This is not to suggest that I would ever advise coding anything whatsoever in C.) Unless... maybe you are saying all the C code in L4 was not actually coded by anybody, but was rather emitted by programs written in these other languages, and L4 is properly a program coded in those languages, with just a transitory C representation on the way to machine code?
- kobebrookskC3 5y agoi wouldn't mind C if every program written in it was written to the standard of seL4, but alas, that isn't the case, and usually it's not even close. i'm also quite sure that getting even close to it would make you want to use another language instead.