3 ms·
The end result is generated C code. So you could simply add the generated C code to the kernel like you would any other C code. And keep the proof chain separat
by mbrodersen 4y ago
The end result is generated C code. So you could simply add the generated C code to the kernel like you would any other C code. And keep the proof chain separate from the kernel. My guess is that it is what Microsoft is doing with the kernel code.
- anitil 4y agoMy question was more around that it would have to replace existing code, so you'd need to advocate for it and come up with some way of incorporating it in the build. I'm not all that familiar with the development culture of the kernel but I imagine that large changes like this would have to be introduced slowly