>But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have No it won't, that's the point.

>But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide. >because it would have far fewer segfaults and the like SEL4 can not segfault, that's the point. It isn't fewer, it is zero. >but clear I was thinking that we can start with a Rust kernel and build on top of that. Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.