> Of course, if it is truly infeasible for any but the least interesting parts of the kernel then it is a waste of time.
I suppose that since there's a high chance of it happening, the question boils down to: "What wins when the decision is between ABI compatibility and provably secure?"