Yeah. I’ve been looking at Idris, Agda and Coq from an arm’s length distance for a while. I actually haven’t heard of the other two. The more formal verification we can insert into our code that gets checked by the compiler the better. The trouble is, the vast majority of the programming community (particularly the web) is only just now realizing the value of types and of pure functions. Getting some of the people I know to even touch something like Scala or Ramda/Sanctuary is like pulling teeth. Getting them to pick up a language like Coq, Agda, or Idris would be damn near impossible. So we have a couple of choices, those of us who do recognize the benefits of provably correct code need to step up and become a culture of doing rather than the culture of ivory tower theory like we tend to have been in the past (comparatively), or we need a substantially better marketing/education process for the languages and toolchains we know provide us these very real world benefits.
