Hacker News Reader

Comment by gsnedders | Hacker News Reader

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!)

View on HN

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:

* Type Theory and Functional Programming (http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/)

* Programming in Martin-Lof type theory (http://www.cse.chalmers.se/research/group/logic/book/)

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.

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.

[1] Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/

Hint: Check out the overview [2] to see the chapter dependencies and decide which chapters you may want to skip.

[2] http://www.cis.upenn.edu/~bcpierce/sf/deps.html

Reply on news.ycombinator.com