[oshepherd]

I love Rust immensely, and it is perhaps my favorite programming language as of late.

However.

This is a microkernel. There is very, very little code inside a microkernel which, if written in Rust, would not end up inside an unsafe block. You are building the safe abstractions here; that code is inherently unsafe.

You could use Rust as a C replacement, but it is a worse C than C, and unsafe rust contains more perils (i.e. UB) than C.

[swetland]

The Magenta kernel is maybe a bit more of a minikernel (97% of drivers and services live in userspace, but the syscall surface provides a wider variety of primitives than just send/recv/exit that a hardcore microkernel design might embrace).

It inherits from LK, which was written in C, but the new surfaces in the Magenta kernel are written in C++ (a restrained, limited C++, intended to take advantage of nice things C++ brings without getting us in too much trouble in the controlled kernel environment).

The core Magenta userspace drivers and services are mostly C at the moment, some will shift to C++ over time, and provided they use the same RPC protocols there's nothing preventing one from building such components in other languages once those other languages are building suitable binaries for Magenta.

[steveklabnik]

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)

[eggy]

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.

[steveklabnik]

  > 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...

[eggy]

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?

[steveklabnik]

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.

[oshepherd]

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.

[steveklabnik]

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.

[Manishearth]

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.

[j-pb]

You could probably write one in forth though ;p, what's good enough for EFI is good enough for the kernel. (You'd end up with a lot of inline assembly probably though, but hey that's less complicated than C++.)

[tmzt]

Did you mean OFW rather than EFI?