Nobody is arguing anything on the level of doing a full on Sel4 -- but Sel4 does have generalized no memory leak, no uaf guarantees as a subset of all specific

Nobody is arguing anything on the level of doing a full on Sel4 -- but Sel4 does have generalized no memory leak, no uaf guarantees as a subset of all specification proofs, so my point "memory safely is possible to bolt onto even C" is still valid.