Is there a port of Redox OS which runs under xen as a guest OS (paravirtual or otherwise)?
Lots of tiny OSes, such as Minix, have been ported to this environment and I think this could be a fun way to run Redox while leveraging the broad device support of a traditional Linux Kernel.
Thanks!
What does work is pretty cool though. Ethernet, input, non-accelerated graphics, nvme and ahci storage
Hang on, I thought the whole point of writing in Rust was that this didn't happen. Is there something about a memory manager that requires unsafe? (Keeping in mind that I neither know Rust nor kernel design, so there's a very good chance that I'm just missing something here)
But yes, memory managers generally require unsafe. Consider what happens when you release memory containing a value of type A, and that memory is later allocated for a value of type B. This is equivalent to a transmute between types A and B, which requires unsafe.
In practice that would mean that you need to write some formal proof, but that doesn't seem impossible. Just like some formal languages require that you write a termination proof to define a recursive function. Of course I'm not saying this is a practical solution for a language like Rust to demand this kind of proofs for every program, but since programs written in a subset of C have been formally verified, it should be possible (and sometimes desirable) for Rust too.
I'm not sure what you mean by ‘borderline magical’. There are formal verification tools for e.g. c and a subset of ada. The sel4 microkernel has been completely formally verified; i.e. it has no unsafe code.
> memory leaks are memory safe in Rust
[1]: https://doc.rust-lang.org/book/ch15-06-reference-cycles.html...
