3 ms·

I don't get your point. They had goals and chose technologies and approaches to achieve those goals. They cite their task model - would you call that some sort

I don't get your point. They had goals and chose technologies and approaches to achieve those goals. They cite their task model - would you call that some sort of 'task evangelism'? They cite that system calls in their OS are synchronous, and how that enables some optimizations that work well with Rust's borrow checker. All of this works together and feels relevant.

CyberRabbi 5y ago
It’s a general talk on OS design centering Rust as a general solution in that space when Rust is just a language not a specific OS design concept or abstraction. The concepts attributed to Rust in this talk can indeed be leveraged in any language (with varying difficulty). The title of the talk says it all: On Hubris and Humility: developing an OS for robustness in Rust Which seems silly to me when this title works just as well: On Hubris and Humility: developing an OS for robustness Now imagine if the title were: On Hubris and Humility: developing an OS for robustness using XML Now I’m sure it’s possible to use XML to develop a robust OS but the usage of XML specifically is less relevant than the techniques employed using XML. In that case the reference to XML seems like evangelism. I’m sure XML evangelism has an audience but it comes across to me as less substantive (and less interesting) than a talk centered around general principles that were successfully leveraged in OS design. It also makes it hard to tell the extent to which the usage of XML specifically to achieve the desired requirements was necessary. A reasonable reader would understand that using the title to make my point is only an example of the content that runs throughout the talk which is similarly oriented around Rust.
- 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 ago
    L4 is coded in C. L4 is proven robust. QED: false.
    - mkj 5y ago
      The 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 ago
        You 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 ago
        i 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.
- staticassertion 5y ago
  But aspects of their OS are clearly intrinsically related to Rust. Like system calls that you can borrow across.
  - CyberRabbi 5y ago
    They’re intrinsically related to having the concept of “borrowing” in some form. Rust is an implementation detail / preference.
    - mlindner 5y ago
      Granted, but do you have another example of a language that does that? I'm not aware of any. If there were then I would think you argument valid.
      - CyberRabbi 5y ago
        You can model borrow semantics relatively easily in both LISP and C++ (and likely countless other contemporary languages) with varying static/dynamic components, it just takes a bit of infrastructure and perhaps some static or dynamic indirection. It’s not “built in” like it is in Rust. The Chromium team did this in C++ as a proof of concept (with notable caveats) somewhat recently: https://docs.google.com/document/d/e/2PACX-1vSt2VB1zQAJ6JDMaIA9PlmEgBxz2K5Tx6w2JqJNeYCy0gU4aoubdTxlENSKNSrQ2TXqPWcuwtXe6PlO/pub https://docs.google.com/document/d/e/2PACX-1vSt2VB1zQAJ6JDMa... Additionally even though this system uses Rust, there is quite a bit of custom support code to coax the system into building for a particular memory-mapping. While you are doing that I don’t see why it wouldn’t be roughly the same amount of infrastructure work in another language. Again, may just require the user to interact with the protected resources through an indirect API instead of language-native constructs but that is more of an ergonomics issue than a feasibility one.
        staticassertion 5y ago
        But... why? Why would they do that? Like why would they go so out of their way not to mention Rust, to the extent that they would discuss borrowing in LISP or C++? That's insanity.

CyberRabbi 5y ago

It’s a general talk on OS design centering Rust as a general solution in that space when Rust is just a language not a specific OS design concept or abstraction. The concepts attributed to Rust in this talk can indeed be leveraged in any language (with varying difficulty). The title of the talk says it all: On Hubris and Humility: developing an OS for robustness in Rust Which seems silly to me when this title works just as well: On Hubris and Humility: developing an OS for robustness Now imagine if the title were: On Hubris and Humility: developing an OS for robustness using XML Now I’m sure it’s possible to use XML to develop a robust OS but the usage of XML specifically is less relevant than the techniques employed using XML. In that case the reference to XML seems like evangelism. I’m sure XML evangelism has an audience but it comes across to me as less substantive (and less interesting) than a talk centered around general principles that were successfully leveraged in OS design. It also makes it hard to tell the extent to which the usage of XML specifically to achieve the desired requirements was necessary. A reasonable reader would understand that using the title to make my point is only an example of the content that runs throughout the talk which is similarly oriented around Rust.

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 ago
  L4 is coded in C. L4 is proven robust. QED: false.
  - mkj 5y ago
    The 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 ago
      You 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 ago
        i 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.
staticassertion 5y ago
But aspects of their OS are clearly intrinsically related to Rust. Like system calls that you can borrow across.
- CyberRabbi 5y ago
  They’re intrinsically related to having the concept of “borrowing” in some form. Rust is an implementation detail / preference.
  - mlindner 5y ago
    Granted, but do you have another example of a language that does that? I'm not aware of any. If there were then I would think you argument valid.
    - CyberRabbi 5y ago
      You can model borrow semantics relatively easily in both LISP and C++ (and likely countless other contemporary languages) with varying static/dynamic components, it just takes a bit of infrastructure and perhaps some static or dynamic indirection. It’s not “built in” like it is in Rust. The Chromium team did this in C++ as a proof of concept (with notable caveats) somewhat recently: https://docs.google.com/document/d/e/2PACX-1vSt2VB1zQAJ6JDMaIA9PlmEgBxz2K5Tx6w2JqJNeYCy0gU4aoubdTxlENSKNSrQ2TXqPWcuwtXe6PlO/pub https://docs.google.com/document/d/e/2PACX-1vSt2VB1zQAJ6JDMa... Additionally even though this system uses Rust, there is quite a bit of custom support code to coax the system into building for a particular memory-mapping. While you are doing that I don’t see why it wouldn’t be roughly the same amount of infrastructure work in another language. Again, may just require the user to interact with the protected resources through an indirect API instead of language-native constructs but that is more of an ergonomics issue than a feasibility one.
      - staticassertion 5y ago
        But... why? Why would they do that? Like why would they go so out of their way not to mention Rust, to the extent that they would discuss borrowing in LISP or C++? That's insanity.