> I found agda much less opaque than coq and especially isabel. Could you explain what you mean by opaque? In Coq you have to memorize a number of tactic names

> I found agda much less opaque than coq and especially isabel. Could you explain what you mean by opaque? In Coq you have to memorize a number of tactic names, and if you don't know the tactics, reading a proof script is useless. And even if you do, it's really hard to reconstruct the proof state in your head from reading the tactic script. So I guess that's "opaque", but I don't see how Agda proof terms are more transparent. I find Isabelle/Isar proof scripts reasonably readable in contrast. But I don't think we have found the good proof assistant yet. (Note to self: Check out Lean already.) EDIT: Ah, forgot about the equational proof style in Agda. That's nice. Pretty much the same is available in Isabelle too. And the niceness breaks down quite quickly: +-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m +-comm′ m zero rewrite +-identity′ m = refl +-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl At this point we're nearing "opaque" territory again.