Hello,

  Agda is essentially an implementation of a type checker for Martin-Lof type theory (i.e. dependent types).

  It is designed to be used as a proof assistant. Roughly speaking propositions are represented as types and a proof of a proposition is a well-typed, total and terminating function. Agda has machinery to help you fill in cases and generally make proof construction easier.

  Agda is different from Haskell in that Agda has dependent types and machinery for interactively constructing the definition of a function at a given type.

  Agda is also different from Haskell in that the focus is on the user interface and writing the proof/program itself, rather than on executing the resulting code (i.e. little work has gone into compiling Agda code).

  I think there have been several projects scattered around on generating Haskell from Agda and on importing Haskell code into Agda for formal verification.

-Jeff

haskell-cafe-bounces@haskell.org wrote on 09/28/2007 11:41:41 AM:

> dons has been posting some links regarding agda on reddit. fairly
> interesting, a quick glance and you think you are reading haskell
> code.
>
> does anyone have any insights on the major differences in these
> languages?
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

---

This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.