<br><font size=2 face="sans-serif">Hello,</font>
<br>
<br><font size=2 face="sans-serif">&nbsp; Agda is essentially an implementation
of a type checker for Martin-Lof type theory (i.e. dependent types). </font>
<br>
<br><font size=2 face="sans-serif">&nbsp; 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.</font>
<br>
<br><font size=2 face="sans-serif">&nbsp; 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.</font>
<br>
<br><font size=2 face="sans-serif">&nbsp; 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).</font>
<br>
<br><font size=2 face="sans-serif">&nbsp; I think there have been several
projects scattered around on generating Haskell from Agda and on importing
Haskell code into Agda for formal verification.</font>
<br>
<br><font size=2 face="sans-serif">-Jeff</font>
<br>
<br><tt><font size=2>haskell-cafe-bounces@haskell.org wrote on 09/28/2007
11:41:41 AM:<br>
<br>
&gt; dons has been posting some links regarding agda on reddit. fairly<br>
&gt; interesting, a quick glance and you think you are reading haskell<br>
&gt; code.<br>
&gt; <br>
&gt; does anyone have any insights on the major differences in these<br>
&gt; languages?<br>
&gt; <br>
&gt; _______________________________________________<br>
&gt; Haskell-Cafe mailing list<br>
&gt; Haskell-Cafe@haskell.org<br>
&gt; http://www.haskell.org/mailman/listinfo/haskell-cafe<br>
</font></tt>
<br>
<span style="font-family:sans-serif,helvetica; font-size:10pt; color:#000000">---</span><br>
<br>
<span style="font-family:sans-serif,helvetica; font-size:10pt; color:#000000">This e-mail may contain confidential and/or privileged information. If you </span><br>
<span style="font-family:sans-serif,helvetica; font-size:10pt; color:#000000">are not the intended recipient (or have received this e-mail in error) </span><br>
<span style="font-family:sans-serif,helvetica; font-size:10pt; color:#000000">please notify the sender immediately and destroy this e-mail. Any </span><br>
<span style="font-family:sans-serif,helvetica; font-size:10pt; color:#000000">unauthorized copying, disclosure or distribution of the material in this </span><br>
<span style="font-family:sans-serif,helvetica; font-size:10pt; color:#000000">e-mail is strictly forbidden.</span><br>