5 ms·

They explicitly justify the lack of solutions for memory safety in their space - both in terms of hardware and software - and why they are building their produc

They explicitly justify the lack of solutions for memory safety in their space - both in terms of hardware and software - and why they are building their product using specific tools. They even note that this may seem like a strange choice (as opposed to using something off the shelf) but that they were willing and able to invest in these tools, specifically that they were going to build pretty much everything from scratch. They even call the project 'Hubris' as a joke about the ambition. Further, they discuss how borrow checking as a model lends itself to the task architecture. It's obviously very relevant. It seems silly to call this evangelism as opposed to a very self-aware deep dive into their choices.

CyberRabbi 5y ago
The abstract software techniques they used to achieve certain properties is more substantial and generally applicable than the specific language they used to instantiate those properties. Citing the language as the causal factor in choosing those techniques and not their requirements is unnecessary evangelism.
- staticassertion 5y ago
  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
- deleted 5y ago
  [deleted]

CyberRabbi 5y ago

The abstract software techniques they used to achieve certain properties is more substantial and generally applicable than the specific language they used to instantiate those properties. Citing the language as the causal factor in choosing those techniques and not their requirements is unnecessary evangelism.

staticassertion 5y ago
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
deleted 5y ago
[deleted]