You can't write a kernel without `unsafe` appearing somewhere.

Yeah. That's why my preferred approach isn't to use Rust for the core TCB. It'd be mostly unsafe anyway, so what's the point? You can write in an all-unsafe language if you want. you can still prove it correct out of band, and seL4 has done that work for you.

Sure, you could just use unsafe Rust and prove it correct with Prusti or something, but why duplicate work?

▲

tadfisher 3 hours ago | parent [-]

I guess then you aren't writing a kernel anymore, you're writing a driver suite for seL4.

	▲	quotemstr 3 hours ago \| parent [-]
		Yep. And that's a good place to be. Keep in mind that the "driver suite" in an seL4 system includes a bunch of things that others would put in the kernel: memory management and swap, networking, filesystems, linking and loading, and so on are all userspace. So, if you want, you still get to differentiate based on interesting low-level things. Calling seL4 system guts a "driver suite" is like calling rustc "just a preprocessor for LLVM IR". True, but only in the most uselessly pedantic sense.