Even when Haskell gets dependent types, they won't be quite as powerful as what agda/coq/idris have with the termination checks I believe. Which is fine, I don'

Even when Haskell gets dependent types, they won't be quite as powerful as what agda/coq/idris have with the termination checks I believe. Which is fine, I don't think that many people want to program via proofs for everything. I'd say Idris is the closest to a useful general purpose programming language with proofs. At least that I've found so far, unless isabelle is? Not used it just came across it a while back and have to have a look. https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html