>It's just, why would you want to edit the proof term manually?
Because you want to produce a particular proof term, because you are programming, not proving. Even with the CHC, there is a distinction between the two.
>Not only do you lose out on information about the generation (Why/How was it generated?), if you change the code it was generated from, you'll have to either manually edit the generated code (especially troublesome because the information of how it was generated was thrown away!)
This is a standard part of programming. Very rarely does editing code come with the complement of how/why the code itself was written - and even it does (like through doc comments) editing the code can then invalidate that information because the motivation can become outdated.
>Tactics aren't 'opaque', it's just a pain to manually look at the generated code and I don't see how the same doesn't apply here.
Because you want to look at the code, because the generated code is the objective of writing the tactics. You are not programming with tactics, you are writing code with tactics.
The point is this: if you wanted to prove `a -> a -> a`, then `intros; assumption` is a fine proof. But if you want to define `min :: (Ord a) => a -> a -> a`, then `intros; assumption` would typecheck without doing what you want. Tactics are not a good fit for programming, in general, because they fit the very different purpose of finding inhabitants rather than specifying them.
By contrast, actually writing code does seem like a good fit for tactics, because the steps you might take to iteratively program the particular term you want fit nicely with individual tactics.