[Haskell-cafe] agda v. haskell

[Jeff Polakow]

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 at 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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070928/c482ce94/attachment.htm