4 ms·

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

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.

tluyben2 13y ago
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.
- jnbiche 13y ago
  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://www.tryidris.org/console http://rise4fun.com/FStar/tutorial/guide http://rise4fun.com/FStar/tutorial/guide
  - tluyben2 13y ago
    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.
  - tluyben2 13y ago
    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 https://github.com/nikswamy/FStar (Apache) https://github.com/idris-lang/Idris-dev https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)
    - dllthomas 13y ago
      coq is LGPL, apparently.
sanderjd 13y ago
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 https://github.com/idris-hackers/idris-crypto - seems like an interesting project.

tluyben2 13y ago

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.

jnbiche 13y ago
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://www.tryidris.org/console http://rise4fun.com/FStar/tutorial/guide http://rise4fun.com/FStar/tutorial/guide
- tluyben2 13y ago
  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.
- tluyben2 13y ago
  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 https://github.com/nikswamy/FStar (Apache) https://github.com/idris-lang/Idris-dev https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)
  - dllthomas 13y ago
    coq is LGPL, apparently.

sanderjd 13y ago

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 https://github.com/idris-hackers/idris-crypto - seems like an interesting project.