[logicchains]

>If Coq's not quite your cup of tea, Isabelle/HOL is another proof assistant with amazing (dare I say superior?) tooling and automation, and it supports code extraction in SML, OCaml, Haskell and Scala.

I'll just note that Isabelle/HOL does not support dependent types, a trade-off it makes in exchange for superior automation (including excellent SMT solver integration). This makes it less suitable for some styles of proving than Coq, Agda, Idris and Lean. I suspect people coming from Coq are less likely to notice this however, as dependent types seem to be used less in Coq than in e.g. Agda or Idris due to the poor support for dependent pattern matching making some things unnecessarily difficult (although this situation is improving with every release).