>Code has a clear context (variables and functions in scope) and a clear goal (return type). At the top level, sure, but if you have a more complex proof term

>Code has a clear context (variables and functions in scope) and a clear goal (return type). At the top level, sure, but if you have a more complex proof term this breaks completely down. You'd have to evaluate potentially arbitrary expressions to determine the types and furthermore there is nothing to indicate the 'human' rather than mechanical structure of the proof since metavariables are just completely gone. It's just not my experience that I could look at a complex proof term (where I don't already know the underlying proof) and figure it out without using an interactive prover. >Add or remove a tactic, and the rest of the proof can be completely invalidated Just like if you randomly removed a part of a proof in term form it wouldn't typecheck anymore? 'stupid' tactics are just as localized as inserting the corresponding term with metavariables . If you're talking about how automation tactics are heavily context dependent, this is more of a fundamental quality of automation rather than tactics. Automation done via reflection suffers from the same issue.