I probably wouldn't until/unless Idris 2 gained some steam, it would probably be Ocaml. I was thinking more along the lines of dependent types, because the kin

I probably wouldn't until/unless Idris 2 gained some steam, it would probably be Ocaml. I was thinking more along the lines of dependent types, because the kinds of problems where you'd really really need strong static types overlap with the need for dependent types, which Haskell has some support for (and Ocaml but less so). But if I needed to prove something I'd probably do it in Coq since it interops with Ocaml fairly well.