I find it interesting that the discussion on Dependent Types lists Idris and Coq as languages and discusses Formal Verification but mostly focuses on Idris and Scala with Shapeless... but to my knowledge, Coq has actually won out in 2019 for this, and Coq has even branded itself for this specifically[0].
I find it interesting that the discussion on Dependent Types lists Idris and Coq as languages and discusses Formal Verification but mostly focuses on Idris and Scala with Shapeless... but to my knowledge, Coq has actually won out in 2019 for this, and Coq has even branded itself for this specifically[0].
[0] https://coq.inria.fr/ - Coq is a formal proof management system.