I am no expert, but Coq and Isabe le "feel" very similar at first, but Isabelle seems to provide much more powerful tools for proof automation than Coq. Isar, I

I am no expert, but Coq and Isabe le "feel" very similar at first, but Isabelle seems to provide much more powerful tools for proof automation than Coq. Isar, Isabelle's proof language, tries to be close to natural language proofs which makes it more intuitive. I really wish Coq had equally powerful automation tools and a more intuitive proof language, because it feels much more of a solid language and I really liked that the clear relation of types <-> statements, terms <-> proofs, type checking <-> proof verification; including the ability to print the raw proof terms of theorems.