>If one wants to have strict guarantees in the form of proofs why not using Agda or Idris instead? Because they're research languages. The amount of non-toy so

>If one wants to have strict guarantees in the form of proofs why not using Agda or Idris instead? Because they're research languages. The amount of non-toy software actually verified in them is zero. I'm not even sure if there's any non-toy software written in Idris besides the Idris compiler itself. Coq's track record is better, but its language is ugly as hell in comparison (and to actually do anything you'd need to extract to Ocaml/Haskell anyway and the same applies to Agda).