Ok- so I know that C is the defacto standard for kernel development. What I'm not saying is that we should all move away from it or that it should be adopted internally. What I am saying is related to security concerns in developing a kernel driver. What may come of it may generally allow for better quality, but that's a separate topic. So kernel programming is very hard. It has both a high bar to entrance and even just getting code to compile and run is not really any guarantee at all that you've done a good job of authoring a kernel driver. I don't really believe that things like Klee really find all errors, but I think that a defense in depth approach would be good. So, when I can get my kernel object to compile, I know that I can test that it runs, but I would also like to have the confidence to know that it won't leak kernel memory or other resources and for that matter will not deference an invalid pointer. Things like Rust allow for better type safety help. In userland programs, SFI is good as a passive backup to type safety but I don't think that SFI is applicable to kernel land because the execution boundaries are not set up under a specific virtual memory scheme. CFI would also be good, but I don't know of any compiler implementation that I can use off the shelf in a kernel programming environment. I guess the best option IMHO is some way to codify the restrictions and semantics of operation somehow into an expressive language that can be checked at compile time. So, in the case of re-entrancy, I'd like an error at compilation time that could just prevent the entrance of bad code. In our case, we'd rather have some good code than a lot of bad code. Does anybody have any recommendations? Or shared interest?