[dmytrish]

Regarding tactics: I started with Coq and I felt for a long time that I had no idea what tactics actually do. Proofs with tactics look nice on the surface, but I really did not like hidden state and hidden actions.

Redoing some proofs in Lean by construction of proof terms was eye-opening, it's just functional programming with dependent types! I still think that teaching with tactics first without exposing proof terms is a mistake.

I've learned to see the value of tactics later, again thanks to Lean: there are proofs that are more natural in the tactics style. Sometimes a mixed approach is ideal: growing intermediate proof terms from the premises and then wrangling the hypothesis with tactics to meet the lemmas.