Hacker News new | ask | show | jobs
by steveklabnik 3602 days ago
Redox is microkernelish, and used to have a lot of unsafe, but has cut it down significantly. You'd be surprised :)

That said, this is pretty much an open research question at this point, so you're right to be skeptical.

(I would also argue that unsafe Rust has more _unspecified_ behavior than C, but not more undefined behavior, but until we get those semantics truly nailed down, can't say for sure. See above "open research question" comment)

2 comments

The LK inner construct is ~15KB. I don't think you could use Rust's safety features and get that size for the LK portion. Maybe the Magenta portion of it though.

"Magenta has a capability-based security model. In LK all code is trusted."

Pony lang is a PL using capability-based concepts too.

  > I don't think you could use Rust's safety features and get that size for the LK portion.
What do you mean? Rust's safety features are mostly compile-time; it shouldn't have implications for binary size. https://github.com/helena-project/tock is an RTOS that runs on an Atmel SAM4L Cortex-M4, and is about ~30kb in size, in my understanding. But that's for the whole OS...
You're right about binary size. I shouldn't have worded it that way.

The point I attempted to make is that when you go small, and pare away what you used to create it, you could have used C and verified it with a certifier/prover. How does Rust address this goal? Truly curious, since I just started learning Rust. I program in C, not C++.

How does your example of the RTOS on the Cortex-M4 at ~30KB compare in complexity to LK at ~15KB in terms of what they deliver in that package size?

I don't know enough about LK to make the comparison.

  > How does Rust address this goal?
Currently? Not as well. There's no total proof framework for Rust yet, it's too early. In a few years? The same way, but with more "proven" by default, without the extra tooling. Tool maturity is certainly one of the areas where C has a leg-up on Rust, by virtues of being decades older.
I took a quick peek at the redox source code and found kernel mode audio and network drivers. This is not a microkernel.

As for UB: Maybe it has less, but that which exists (e.g. noalias on mut refs) is very dangerous.

Yes, they're in the middle of some refactoring stuff; they had to put some things back in the kernel. Should be back out when they're done.
No more dangerous than existing UB in C, just that we're not used to it. And it's easy to disable for your types.

Like Steve said, the exact nature of this UB isn't completely specified yet (as in, when it actually is UB), so it is dangerous right now, but that's just temporary.