> 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.
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.