I haven't had the chance to watch the two videos yet, but at BFPG (2015-03), Matthew Brecknell did an "Introduction to Agda" talk that might also be interesting to some.
Agda, Coq etc is something I really want to learn someday. I'm already pretty proud that I finally can write some haskell, but this stuff is next level. I might give Idris a go first though, as it seems very similar to haskell in syntax.
With Agda, I found that understanding the dependent type system, the basics of proofs, and why the Curry-Howard equivalence holds, was all pretty easy. It makes sense—it's, uh, logical. The Emacs mode for it is like a gamification of deductive reasoning; very fun.
Then grokking the module system and the basic proof tools in the standard library, that was a little hurdle. I spent a weekend writing up some basic definitions from group theory, and it was a lot like learning some other language, confusing at times and requiring trial and error. Very worth the effort!
I think the basic insight behind the Curry-Howard thing can be indicated very simply. A function type "A -> B" says that given some arbitrary A, you can come up with an element of B. In other words, "forall A there exists a B".
For this to actually hold, the language needs to prevent cheating, i.e., prevent terms having type X that don't actually evaluate to an X — like Haskell's error function which has type "forall x. String -> x", or infinite recursive definitions like "x = x".
Dependent typing is simple too. It just means that the types are made up of first-class values no different from expression values. You can't reasonably do this in Haskell because Haskell's expression values aren't guaranteed to terminate, and a type checker should terminate.
I'd love to use such a language for modelling the domain logic of programs, but I never got further than experimentation.
The function type A -> B corresponds to A => B in logic. This is a subtle but important difference between logic and type theory. In logic a statement is true or false, but that's it. In type theory a statement (= type) has evidence (= values of that type). The type A -> B can be interpreted as turning evidence for A into evidence for B.
The logical statements "for all x:A it's the case that B(x) holds" and "there exists a x:A such that B(x) holds" correspond to dependent function types `(x:A) -> B x` and dependent pair types `(x:A, B x)`, respectively. In intuitive terms "if you give me an x:A, then I give you evidence of B(x)", and "I give you an x:A, along with evidence of B(x)".
https://www.youtube.com/watch?v=QyUVONbwHYE
https://www.youtube.com/watch?v=7iAkFh9xOIc