In what programming language would you write new OS?
In your opinion what programming language should be used to write a new operating system for the 21 century?
But, what would be your design criteria for the new language?
I'd aim for somewhere between Rust and <other_imperitive_languages>.
I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention. Something like C, but with markup describing data lifetimes, value ranges, permissible access, etc.
The guys at Bungie did something similar for Destiny: https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s
There are also some PHd folks working on adding type annotations to C and restricting aliasing rules. Those annotations/rules get fed through a solver that proves it's free of latent memory bugs. As far as I remember they're trying to prove the Android thread scheduler. I couldn't find the talk/slides, but it turns out that's hard in C, but with a brand new language you could probably do it pretty easily (easily being a few man-years, instead of tens of).
>> I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention.
For "provably correct programs", the "<other_imperative_language>" could be SPARK:
https://learn.adacore.com/courses/intro-to-spark/chapters/01...
If you wait a bit, Ferrocene may be what you are looking for:
You don't need as much unsafe as you think, especially for "optimization."
Rust is still backward compatible (old code will compiles on newer compiler versions) so you won't be rewriting what already works.
You won't use unsafe that much (especially once the hardware parts have been abstracted), see the link I gave you as proof.
The advantages of Rust are not pointless:
- the type system
- the ownership/borrowing/move semantics
- the ecosystem
- the build system
- the way you can contain the memory-unsafe parts in a small/controlled API
Just to clarify, when I say the OS, Im going with the definition of Linux Kernel being the actual OS, with other stuff on top of it comprising the rest of the system. The core kernel should absolutely be written in C, with careful attention to detail. The rest of the OS is totally fine to use Rust (or really any other language). Which is pretty much the direction Linux is going. The core kernel will still use C because its the most stable syntax currently in existence, while module development will allow Rust.
There has been efforts to write drivers in Rust for things like NVME (https://www.phoronix.com/news/LPC-2022-Rust-Linux), which required a lot of work, and guess what, plenty of `unsafe` scattered through the implementation. Yes, it made the implementation easier, but that is one of the major problems. As long as Rust allows this, you won't have safe code. And without it, things will take much longer to write, likely be slower without careful design, which means less adoption. Its a Catch 22 really, since less adoption means less development, but nevertheless, getting rid of unsafe is absolutely necessary if you want Rusts safety features to work.
Also to address your advantages of Rust, C has a type system, its just is very open and has less semantics (as it should, so that the software doesn't do its ow aren't clearly stated by the developer). It also has an ecosystem (LLVM/Clang, GCC, libc, all the standard libraries in the linux kernel). You generally also don't want a package manager for something that you write an OS in, considering all the exploits that happen with pip/npm and malicious packages. C also has a very good build system (CMake/Scons), and plenty of memory safety built into core functions.
Re: unsafe, there's a similar objection/question that comes up frequently. The Rust standard library is full of unsafe code, as are a lot of common foundational crates. Doesn't that mean that most Rust applications are vulnerable to memory corruption bugs?
The short answer is that safety in Rust isn't about having proofs of correctness all the way down. (Some people do that, but they're inscrutable wizards, and I try not to meddle in their affairs.) Instead, it's about having robust and useful ways to encapsulate unsafety. You want to be able to say "if this function is correct, then callers can't use it to corrupt memory no matter how hard they try." Rust gives you ways to achieve that, without paying the cost of a garbage collector or a GIL.
In embedded/OS development, the difference is that the big pile of unsafe code underneath is probably written by you instead of by compiler folks. That certainly isn't easy. But the tools for encapsulating it are the same, and the value proposition is the same.