3 ms·

There's Redox, which is progressing nicely, already boots in a VM and on some real hardware, and has a GUI and networking, and is intended to be a real general

There's Redox, which is progressing nicely, already boots in a VM and on some real hardware, and has a GUI and networking, and is intended to be a real general purpose OS someday. There's also intermezzOS, which is a (still being written) "build-your-own-OS" tutorial project that uses Rust. It's also worth noting that Rust isn't magic and especially when doing very low-level stuff the use of unsafe blocks is unavoidable. On the other hand, by isolating unsafe behavior you know where it is and can test it very carefully and keep it as contained as possible.

DaiPlusPlus 9y ago
As more people use Rust and we see all the cases where unsafe is typically used, could more unsafe code patterns be formalized as safe code? Are there any situations where unsafe code cannot be avoided at all, where there exists a program-theory proof that unsafe code must be used? If it's for performance reasons, then a new safe language construct could be introduced to replace it - such as how a safe range-based loop eliminates the need for bounds-checking with fixed-length arrays.
- apendleton 9y ago
  For many uses this is already happening, but for writing an OS, there's no getting around the fact that you're going to need to, say, write to or read from a specific hard-coded memory address that, for a given platform, is magically mapped to a hardware register. That's always going to be unsafe. Certainly, though, Rust lets you sequester that kind of code away and isolate it from things that can be expressed safely.
  - nickpsecurity 9y ago
    I'll add that there's already tooling in Frama-C, SPARK Ada, and some proof assistants to prove safety of some of those operations. So, if they can't be safe, then a mock-up of them can be done in something that can prove their safety externally with proven component integrated into Rust. Eventually Rust itself might have such a capability but the external tools can work intermediate.

DaiPlusPlus 9y ago

As more people use Rust and we see all the cases where unsafe is typically used, could more unsafe code patterns be formalized as safe code? Are there any situations where unsafe code cannot be avoided at all, where there exists a program-theory proof that unsafe code must be used? If it's for performance reasons, then a new safe language construct could be introduced to replace it - such as how a safe range-based loop eliminates the need for bounds-checking with fixed-length arrays.

apendleton 9y ago
For many uses this is already happening, but for writing an OS, there's no getting around the fact that you're going to need to, say, write to or read from a specific hard-coded memory address that, for a given platform, is magically mapped to a hardware register. That's always going to be unsafe. Certainly, though, Rust lets you sequester that kind of code away and isolate it from things that can be expressed safely.
- nickpsecurity 9y ago
  I'll add that there's already tooling in Frama-C, SPARK Ada, and some proof assistants to prove safety of some of those operations. So, if they can't be safe, then a mock-up of them can be done in something that can prove their safety externally with proven component integrated into Rust. Eventually Rust itself might have such a capability but the external tools can work intermediate.