> 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

> 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. That's what the GIF at the top of the article shows: The two choices are 1. Attempt to fill hole 2. Introduce lambda The user types "1" and the rest happens automatically. > 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 The interface suggests that you won't need to recall that you need "homo"; it'll be presented as one of several possible choices and you only need to recognize that this is the choice you want (or not).