13 ms·
We have been in contact with a set of companies and academia members that would like to use Rust as a second language in the kernel. Some of them have alrea
by 0x008 5y ago
We have been in contact with a set of companies and academia members
that would like to use Rust as a second language in the kernel. Some
of them have already started to evaluate Rust for their needs using
the infrastructure we have already in place.
In particular, we have got a few statements from major companies.
In no particular order:
Microsoft's Linux Systems Group is interested in contributing to
getting Rust into Linux kernel. Hopefully we will be able to submit
select Hyper-V drivers written in Rust in the coming months.
Arm recognises the Rust value proposition and is actively working
with the Rust community to improve Rust for Arm based systems.
A good example is Arm’s RFC contribution to the Rust language which
made Linux on 64-bit Arm systems a Tier-1 Rust supported platform.
Rustaceans at Arm are excited about the Rust for Linux initiative
and look forward to assisting in this effort.
Google supports and contributes directly to the Rust for Linux
project. Our Android team is evaluating a new Binder implementation
and considering other drivers where Rust could be adopted.
In addition, IBM contributed the Rust kernel support for PowerPC
which was already included in the RFC.
- transitory_pce 5y agoEvery one of these companies except has a competing OS. Just saying.
- rvz 5y ago'except' Who? ARM? Well [0] [0] https://github.com/ARMmbed/mbed-os https://github.com/ARMmbed/mbed-os
- pjmlp 5y agoAlso to note, ARM toyed with the idea of using a Linux distribution as alternative to MBed, but it was short love, it is already dead, it only lasted one release. https://os.mbed.com/docs/mbed-linux-os/deprecated-product/welcome/index.html https://os.mbed.com/docs/mbed-linux-os/deprecated-product/we...
- _wldu 5y agoAll of them are interested in good technical security (actually being secure).
- grumblenum 5y agoSo why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-Star)? Or a language with good performance and a verified subset (Ada/Spark)? I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.
- kaba0 5y agoFormal verification techniques don’t scale, not even to your average CRUD app, let alone to an OS-scale.
- hulitu 5y agoTesting is hard. And (very) expensive.
- kaba0 5y agoFormal verification is even harder. And even more (very) expensive.
- tonyarkles 5y agoIn a number of ways I'd argue that FV of an average CRUD app is a very hard problem, for two reasons: - the requirements generally change quite frequently - the requirements are generally a long way from being "formally verifiable" Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work: - A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states. - A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases. - Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.
- wongarsu 5y agoHaving Linux make the first move, then learn from their successes and mistakes to implement a better version in your own OS seems like a good move that profits everyone. It's not like Microsoft isn't pushing Rust on their own platform. Every time a Windows driver does a use-after-free somebody swears at Microsoft for causing a bluescreen.
- cogman10 5y agoFrom what I've heard (3rd hand :D), Rust has already made it's way into the windows kernel.
- yawaramin 5y agoLinux isn't an OS and every one of them relies on it for mission-critical infrastructure.
- pjmlp 5y ago> Microsoft's Linux Systems Group is interested in contributing to getting Rust into Linux kernel. Hopefully we will be able to submit select Hyper-V drivers written in Rust in the coming months. At very least the Azure Sphere OS team should finally adopt Rust, instead of doing security marketing with the 7 layers of whatever, and then shipping a C only SDK. It is like they are absent of the company security efforts, while trying to sell us a story of how much they care about security.
- somebody_amzn 5y agoAzure Sphere OS was designed to fit in a 4MB of SRAM envelope... while actually using a Linux kernel. If I remember well, only 512KB is actually usable by OEM applications on that platform.
- pjmlp 5y agoAnd? I was using C++ on MS-DOS. Not even C++ is supported on the Azure Sphere OS SDK. Ironically they usally tend to evade the question when asked about it, to the point they ended up writing a very long blog post trying to justify C, and it had nothing to do with space requirements. Rather industry expectations and other marketing speak.
- somebody_amzn 5y agoThe libc and libraries that they already add to apps don't leave enough space for an off-the-shelf C++ runtime to be included. So instead of including a custom runtime they just bailed out...
- ksec 5y agoI never quite understood why Ada/Spark dont get the same attention or love.
- programmer_dude 5y agoAda syntax is too verbose.
- MaxBarraclough 5y agoAda deliberately places readability before writeability. It's interested in the maintainability of large mature programs, and isn't intended for rapid application development. I don't have enough experience with Ada to comment on whether its verbose and keyword-heavy syntax succeeds in this goal.
- zerr 5y agoCode is not a prose. C-like syntax is much easier to read compared to Ada/Pascal's text blobs.
- oblio 5y agoAccording to studies which we have none of right now. So that's like... your opinion, man.
- zerr 5y agoBesides, if the prose would have been preferable over symbols, we'd be writing e.g. "an unknown number of apples summed up with an unknown number of pears equals to one hundred entities" instead of "x + y = 100" in math classes :)
- MaxBarraclough 5y agoThat's a caricature. We sometimes use words for summation, e.g. Python's sum and fsum functions. I do wonder though if people had to write like that before the development of modern mathematical syntax. Even the '=' symbol is relatively young. Wikipedia tells me it was invented in 1557. SQL is another 'wordy' language. There are many, many things wrong with the SQL language, but I wouldn't say its wordiness is one of them.
- mapgrep 5y agoFunnily similar wording to an old slashdot troll message about rewriting the Linux kernel in Visual Basic: “I hope to see a switch from C to VB very soon. I've already spoken with various luminaries in the C coding world and most are eager to begin to transition. Having just gotten off the phone with Mr. Alan Cox, I can say that he is quite thrilled with the speed increases that will occur when the Linux kernel is completely rewritten in Visual Basic. Richard Stallman plans to support this, and hopes that the great Swede himself, Linux Torvaldis, won't object to renaming Linux to VB/Linux. Although not a C coder himself, I'm told that Slashdot's very own Admiral Taco will support this on his web site. Finally, Dennis Ritchie is excited about the switch!”
- Igelau 5y agoDid Netcraft confirm it?