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.
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.
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.
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?
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.
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-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.
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++?
At this point, I have lost track of your argument. Do you object to Hubris being written in Rust or do you object to Cliff explaining why Hubris is written in Rust?
I don’t object to Hubris being written in Rust, that would be silly. My argument is really simply my opinion that the talk would have been more interesting if it were less focused on how Rust was used to make Hubris and more focused on how specific high level software techniques and concepts were used to make Hubris.
I don’t really need a long winded justification for why this is written in Rust. Everyone knows that ultimately comes down to a mix of personal preference and tool availability. I can fill in the details myself how the high level software techniques presented would map to Rust constructs.
I'm not sure what you can really accuse of being long-winded here, but it's clear that the presentation hits a nerve for you, so probably best left at that.
All of this works together and feels relevant.