Well, in part because they don't document the context and the goal. Code has a clear context (variables and functions in scope) and a clear goal (return type). Editing code vs tactics is easy because the impact that each edit has on the context, goal, and code is clear and localised. Add or remove a tactic, and the rest of the proof can be completely invalidated.

The fact that you can look at a code snippet and tell what it does, but looking at a tactic snippet essentially tells you nothing, is exemplary of the difference. Just the fact that you need a more powerful editing tool (interactive provers) to edit tactic proofs at all is testament to how much more complicated they are.

>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.