Hacker News Reader

Comment by ramidarigaz | Hacker News Reader

Relevant: I attended LambdaConf yesterday at CU Boulder, and there was a _great_ intro workshop for Idris, which is in the same domain as Coq. Idris is similar to Haskell (it's actually written in Haskell), but with a dependent type system, a tactic-based theorem prover like Coq has, and a bunch of other fun features.

View on HN

Idris is really worth checking out if you have any interest in this kind of stuff. I used Coq and now am playing with Idris and F*; the latter two feel good and practical. With an FP background they are easy to pick up.

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:

http://www.tryidris.org/console

http://rise4fun.com/FStar/tutorial/guide

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;

https://github.com/nikswamy/FStar (Apache) https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)

coq is LGPL, apparently.

Another relevant shout-out for LambdaConf and Idris: Greg Pfeil gave a lightning talk on his preliminary work using Idris for proven crytpo primitives - https://github.com/idris-hackers/idris-crypto - seems like an interesting project.

Reply on news.ycombinator.com