This is really incredible work, wonderful in fact, but at the same time it simply excites me for tools that go further. Having to key in the correct tactic to

This is really incredible work, wonderful in fact, but at the same time it simply excites me for tools that go further. Having to key in the correct tactic to fill in a program still involves the same actions required by typing a program as text namely thinking (identifying which tactic is the correct one) and typing (keying in the tactic). A system that “derives the obvious functor for a data type automatically”, permitting overrides would be more useful. For most programers the ROI on learning tactics isn’t that high. It effectively entails encoding the basic things they already understand like pattern matching into more abstract jargon that, while more general, requires further study to use properly. Most of the time, especially for complex cases, it will be faster and lower effort to just write the pattern match yourself rather than have to think in terms of sequences of abstract operations and recall that “oh I need ‘homo a b’, ‘refl’ here or w/e (some might disagree, but I find thinking in terms of concrete matching on symbols is much easier than thinking in terms of sequences of tactic/proof operations, recalling what they do, etc.) For this reason, I personally don’t think programing with theorem proving/tactics will take off until the basic derivations are entirely automatic and tuning them to a complex or custom use case is a matter of easily retyping one or two proof lines.