I think one of the biggest barriers to formal verification is that it is, for lack of a better term, "too formal". There's a bunch of other terminology, language, etc. you have to learn, and the learning curve is steep. For someone who just wants to prove a few pre/post-conditions on some functions (that's why I looked into Coq originally - and gave up because it was too hard), it's too much. There is a feeling that it is too theoretical. I eventually found it easier to prove what I needed to, manually.
Bingo, unfortunately. I've been able to learn functional programming in Haskell and OCaml without any formal academic background, but looking at Coq, Agda, Idris, and F*, I despair of learning them without more accessible tutorials or a PhD in computer science concentrating on type theory.
My first intro to Haskell was through "Learn you a Haskell". I think without that type of introduction, I never would have progressed past basic pattern matching and folds/maps/filters. I need something similar for dependent typing.
There's Learn You An Agda at <https://github.com/liamoc/learn-you-an-agda>, though it never got that far. (I've done comparatively little with theorem provers (v. model checkers), so I can't point you anywhere that useful!)
All these tutorials won't teach you how to use coq or agda. The main problem is that in order to use coq or agda, you need to learn Martin-Lof type theory (or calculus of inductive constructions, which is a similar formalism to MLTT) first, and learn to write code later. Otherwise everything will seem like a magic. There are however, good books on the topic:
There's a really wonderful tutorial on Coq [1] that holds your hand through all the theory you need to learn. I took a class that used this tutorial and I found it to be very understandable and practical, with hardly any background on formal methods myself. Yes, it's a steep learning curve, but at least with this tutorial, you know the curve you need to follow.
But Haskell is also based on some type system, and yet Learn You a Haskell teaches Haskell without formally teaching this type system.
I've been learning Idris and reading the HoTT book at the same time. I'm not sure what it would have been like learning Idris without any formal type theory, but I believe it would be possible.
The difference here is that type system in case of agda and coq is the core of the language, it's very similar to what operational semantics does with usual programming languages. The type systems is a logic via Curry-Howard correspondence, with which program correctness is proved. In case of Haskell it's just a software engineering tool which helps you find errors in your program in a semi-automatic way.
I would say its a sliding scale, I don't think there is a sharp qualitative difference between Idris and Haskell. Haskell programs can also be thought of as proofs, namely proofs that the variables/functions you define have the types you claim they have.
You mention Agda and Coq. Maybe one difference in our viewpoint is that Idris really is designed for general purpose programming. E.g. you can write a program with almost identical structure to a Haskell program.
>I don't think there is a sharp qualitative difference between Idris and Haskell.
Yes, there's no such a difference. However, in order to use Idris to its full potential, you need to use dependent types. It's just like writing procedural programs in object-oriented or functional language. It's possible, however, it's not a very bright idea.
