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.