I enjoy programming in Agda as well. However I can’t decide whether to focus on Agda, Idris, LEAN, Coq, F* or Isabell/HOL. There is a lot of overlap but none of

I enjoy programming in Agda as well. However I can’t decide whether to focus on Agda, Idris, LEAN, Coq, F* or Isabell/HOL. There is a lot of overlap but none of those choices seems to have it all.