[Gajurgensen]

I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn't infer (or which we just don't wish to delegate). Things like "induct according to this scheme after generalizing this variable" or "first prove this auxiliary lemma" or "apply this inverse function to both sides so that they cancel".

I'd also argue that automation is essential to practical proof engineering. It make the proofs less brittle to minor changes and therefore more maintainable.

Edit: a couple more thoughts. First, there is nothing stopping you from defining proof objects directly in Lean without tactics. That flexibility is quite nice -- you can automate as much or as little as you like. Of course, in practice, people almost always use tactics. Second, I use the ACL2 prover quite a bit, which is not tactic-based. Instead, you give high-level "hints" that steer the aggressively-automated prover. Funny enough, I have colleagues that look at Lean proofs and say "these proofs are so verbose, how does anyone understand them!".

[black_knight]

I feel like there is a lot of interesting things one can do in proof engineering without resorting to "tactics" (meta-programs searching for the proof). In some cases one can replace them by robust lemmas which show general results. Or the language could have good support for abstractions (dependent types already give us a lot of power here!).

Personally, I am experimenting a lot with Agda's instance arguments these days. They somehow have a bad rep for being slow, but their performance has improved a lot! One can juice it to write really readable code (Like truly ad-hoc polymorphic operators, or declaring axioms used in a theorem like `⦃ AC ⦄ → Theorem`), but it also allows for proof searches. Contrary to “tactics”, instance arguments feel like a fluid part of the proof language.

I think there is a lot of room for innovation in the space of proof engineering. I really hope that LLMs will not suck all the oxygen out of the room, by being trained on existing dogmas.

[derdi]

Very well put. I'll just add that there is one more thing one can do to document the important/insightful/interesting parts of a proof, where it makes sense: Write a comment.