[pmahoney]

The article covers this here http://williamdemeo.github.io/2014/02/27/learn-you-an-agda/#...

Some excerpts:

> Agda is a programming language that uses dependent types ... you can actually include values inside a type. For example, the List type constructor can be parameterized by both the type of its contents and the length of the list in question ... . This allows the compiler to check for you to make sure there are no cases where you attempt to call head on a potentially empty list, for example.

> If I can come up with a function of type Foo -> Bar (and Agda says that it’s type correct) that means that I’ve written not only a program, but also a proof by construction that, assuming some premise Foo, the judgment Bar holds.

> Proofs work in concurrent scenarios. You can’t reliably unit test against race conditions, starvation or deadlock. All of these things can be eliminated via formal methods.

> Thanks to Curry-Howard, Agda can also be used as a proof language, as opposed to a programming language. You can construct a proof not just about your program, but anything you like.

[lmm]

Is there a comparison to Idris? It sounds like they're very similar, and more of the people I've followed seem to be interested in Idris than Agda.