I've also been playing around with these two. I have a little Haskell and some OCaml, but very little understanding of the mathmatics involved in dependent typing, so I'm struggling but still very interested. Wish there were an accessible guide like "Learn you a Haskell" for Idris.
By the way, for anyone interested in these two languages with dependent typing, you can try out both Idris and F* online, without installing anything:
My background is theoretical CS (2 of my professors were pupils of Dijkstra and they were quite particular about formal verification as you can imagine) so that helps; it's good for anyone with an interest in this to read books like 'A discipline of programming' by Dijkstra or more modern books about it (and if you really like it, continue on to Pierce who is the types guy and when I read his some of his work the first time I kind of wondered wth we were doing in programming while this guy already figured it out to such an extent ;).
It all starts to make more sense after some of the theoretical basis. I guess; I don't know how much years of writing formal proofs on pen & paper 20 years ago influenced me in reading this stuff.
Cannot edit for reason, but I thought I would mention, as this is of vital importance to me when i'm learning something new, that both Idris and F* are open source;
By the way, for anyone interested in these two languages with dependent typing, you can try out both Idris and F* online, without installing anything:
http://www.tryidris.org/console
http://rise4fun.com/FStar/tutorial/guide