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.