I agree. Note that the Coq-style tactics-based approach is not the only possibility. In Agda, you are expected to write proofs in a functional style, similar

I agree. Note that the Coq-style tactics-based approach is not the only possibility. In Agda, you are expected to write proofs in a functional style, similar to Haskell programs. There is a small amount of integrated automation, which helps you fill in holes in your proofs — however, the results are explicit proof terms, inserted at the right place in your program. Systems which behave in this fashion have the de Bruijn criterion, as described in Geuvers (2009) “Proof assistants: History, ideas, and future”. https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf