Comment by why_only_15
21 hours ago
To what degree can you say something like "if the kernel doesn't have metaprogramming [or some other set of features] it's fine". When were the last bugs with a reduced feature set?
21 hours ago
To what degree can you say something like "if the kernel doesn't have metaprogramming [or some other set of features] it's fine". When were the last bugs with a reduced feature set?
Read the article. The elaborator (where metaprogramming is evaluated) is not part of the trusted computing base. The security model is that bad proof terms get rejected, not that they're never generated.