[cpach]

I’m just a layman when it comes to these kind of things. But here’s my take anyway: AFAICT, the issue isn’t so much about rewriting the code. However, if we would use automation for that, we would probably need proofs that the new code is better than the old one. And creating suchs proofs seems incredibly hard as soon as we walk out of “hello world” territory. People has spent years on trying to make suchs systems, but it’s still not widely used. So until then, we need people who read and analyze the code, and also have wast knowledge of the kernel’s inner workings, and today that seems to be the bottleneck. Those people doesn’t really grow on trees.