> Are you suggesting that the error rate of type checkers, verified or not, is even in the same ballpark as the error rate of human reviewers?
Nope, but your unqualified statement was simply false, and in any case, your point isn't really relevant. This single line of code we're discussing is easily verifiable by manual inspection and automated testing. We're not talking about huge swaths of code here, we're talking about a few unsafe primitives, because this kind of reuse isn't typical of a microkernel.
The type safety of a single operation expressed as a template is relatively insignificant compared to the added complexity of C++, particularly considering the "reuse" benefits are non-existent for microkernels, and if all you're left with is some elusive "type safety" for a linked list, that's simply not enough.
This is obvious when you know the history of multiple C++ kernel verification efforts, all of which failed, no matter how simple of a C++ subset was chosen. Many C verification efforts have succeeded, and tools for lightweight formal methods, like Frama-C, make the transition to verification possible with C. C++ is a dead end for this purpose, and the various L4 groups that created L4 kernels in C++ and then rewrote them in C all agree.