4 ms·

I'll have a look thanks but note that seL4 is implemented in C because C has a formally verified compiler CompCert which Rust doesn't have..

• steveklabnik 6y ago
  ... not to mention that seL4 was started in 2006, a full four years before Rust was even conceived of. The proof was finished a year before.