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

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.