Original HN discussion (linked at top of article as well): https://news.ycombinator.com/item?id=7565153 https://news.ycombinator.com/item?id=7565153 I find it

Original HN discussion (linked at top of article as well): https://news.ycombinator.com/item?id=7565153 https://news.ycombinator.com/item?id=7565153 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/ https://coq.inria.fr/ - Coq is a formal proof management system.