<div dir="ltr">I have a newbie question.... Does theorem proofs have a use for an application? Take for example the IRC bot example (<a href="http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot">http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot</a>) listed below. Is there any insight to be gained by theorem proofs (as in COQ) into the app? <br>
<br>Thanks,<br><br>Daryoush<br><br><div class="gmail_quote">On Sat, Sep 13, 2008 at 4:07 PM, Brent Yorgey <span dir="ltr"><<a href="mailto:byorgey@seas.upenn.edu">byorgey@seas.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
---------------------------------------------------------------------------<br>
Haskell Weekly News<br>
<a href="http://sequence.complete.org/hwn/20080913" target="_blank">http://sequence.complete.org/hwn/20080913</a><br>
Issue 85 - September 13, 2008<br>
---------------------------------------------------------------------------<br>
<br>
Welcome to issue 85 of HWN, a newsletter covering developments in the<br>
[1]Haskell community.<br>
<br>
Announcements<br>
<br>
citeproc-hs. Andrea Rossato [2]announced the first release of<br>
[3]citeproc-hs, a Haskell implementation of the [4]Citation Style<br>
Language. citeproc-hs adds a Bibtex-like citation and bibliographic<br>
formatting and generation facility to [5]Pandoc.<br>
<br>
Twidge. John Goerzen [6]announced the release of [7]Twidge, a<br>
command-line Twitter and Identi.ca client.<br>
<br>
Real World HAppS: Cabalized, Self-Demoing HAppS Tutorial (Version 3).<br>
Thomas Hartman [8]announced a new version of [9]happs-tutorial, with a<br>
correspondingly updated [10]online demo.<br>
<br>
generic list functions fixed. Jim Apple reported that genericTake,<br>
genericDrop, and genericSplitAt have [11]been fixed so they are now<br>
total functions (they used to fail on negative integer inputs, unlike<br>
their ungeneric counterparts).<br>
<br>
The Monad.Reader (13) - Call for copy. Wouter Swierstra [12]announced a<br>
call for copy for Issue 13 of the [13]Monad.Reader. The deadline for<br>
submitting articles is February 13, 2009.<br>
<br>
Heads Up: <a href="http://code.haskell.org" target="_blank">code.haskell.org</a> is upgrading to darcs 2. Duncan Coutts<br>
[14]announced that /usr/bin/darcs on <a href="http://code.haskell.org" target="_blank">code.haskell.org</a> will soon be<br>
upgraded to version 2. Most users should be unaffected as darcs 2 works<br>
just fine with repositories in darcs 1 format, and has been extensively<br>
tested for correctness.<br>
<br>
Discussion<br>
<br>
packages and QuickCheck. Conal Elliott [15]asked what methods of<br>
organization people use to package up QuickCheck tests for their<br>
libraries.<br>
<br>
Hackage needs a theme song!. Jason Dagit wrote a [16]theme song for<br>
Hackage!<br>
<br>
Jobs<br>
<br>
Gamr7. Lionel Barret De Nazaris [17]announced that [18]Gamr7, a startup<br>
in France focused on procedural city generation for the game and<br>
simulation market, is looking for a senior developer/technical<br>
director.<br>
<br>
senior role at Credit Suisse. Ganesh Sittampalam [19]announced that<br>
[20]Credit Suisse is seeking to recruit an expert in functional<br>
programming for a senior role in the Global Modelling and Analytics<br>
Group (GMAG) in the Securities Division.<br>
<br>
Blog noise<br>
<br>
[21]Haskell news from the [22]blogosphere.<br>
* Douglas M. Auclair (geophf): [23]What is declarative programming?.<br>
* John Goerzen (CosmicRay): [24]New Twitter Client: Twidge.<br>
* Mark Jason Dominus: [25]Return return. Mark's mind is blown by the<br>
code "return return" appearing in a paper by Mark Jones.<br>
* Eric Kow (kowey): [26]darcs weekly news #3.<br>
* Ketil Malde: [27]The FastQ file format for sequences.<br>
* >>> Nathan Sanders: [28]Real World Haskell. Nathan experiments with<br>
porting some of his Python code to Haskell.<br>
* Andrea Vezzosi (Saizan): [29]Results from GSoC. Andrea's GSoC work<br>
on a high-level dependency framework for Cabal is going to be<br>
released in a separate package for now, [30]hbuild.<br>
* >>> Ricky Clarkson: [31]An IRC Bot in Haskell, 20% code, 80% GRR.<br>
Ricky shares his experiences, frustrations, and eventual success<br>
writing a simple IRC bot in Haskell.<br>
* >>> Yaakov Nemoy: [32]Xmonad 0.8 released.<br>
* Luke Palmer: [33]The problem with Coq. ...is, according to Luke,<br>
that it doesn't have a nice graphical interface.<br>
* >>> James Cowie: [34]Haskell! yes no?. James dives into learning<br>
some Haskell. Verdict so far: a "very nice language".<br>
<br>
Quotes of the Week<br>
<br>
* EvilTerran: this is hard to express in this type system. i'm going<br>
to make my own type system instead!<br>
<br>
About the Haskell Weekly News<br>
<br>
New editions are posted to [35]the Haskell mailing list as well as to<br>
[36]the Haskell Sequence and [37]Planet Haskell. [38]RSS is also<br>
available, and headlines appear on [39]<a href="http://haskell.org" target="_blank">haskell.org</a>.<br>
<br>
To help create new editions of this newsletter, please see the<br>
information on [40]how to contribute. Send stories to byorgey at cis<br>
dot upenn dot edu. The darcs repository is available at darcs get<br>
[41]<a href="http://code.haskell.org/%7Ebyorgey/code/hwn/" target="_blank">http://code.haskell.org/~byorgey/code/hwn/</a> .<br>
<br>
References<br>
<br>
1. <a href="http://haskell.org/" target="_blank">http://haskell.org/</a><br>
2. <a href="http://article.gmane.org/gmane.comp.lang.haskell.cafe/44471" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.cafe/44471</a><br>
3. <a href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/citeproc%2Dhs" target="_blank">http://hackage.haskell.org/cgi-bin/hackage-scripts/package/citeproc%2Dhs</a><br>
4. <a href="http://xbiblio.sourceforge.net/csl/" target="_blank">http://xbiblio.sourceforge.net/csl/</a><br>
5. <a href="http://johnmacfarlane.net/pandoc/" target="_blank">http://johnmacfarlane.net/pandoc/</a><br>
6. <a href="http://article.gmane.org/gmane.comp.lang.haskell.cafe/44453" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.cafe/44453</a><br>
7. <a href="http://software.complete.org/twidge" target="_blank">http://software.complete.org/twidge</a><br>
8. <a href="http://article.gmane.org/gmane.comp.lang.haskell.cafe/44410" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.cafe/44410</a><br>
9. <a href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/happs-tutorial" target="_blank">http://hackage.haskell.org/cgi-bin/hackage-scripts/package/happs-tutorial</a><br>
10. <a href="http://happstutorial.com:5001/" target="_blank">http://happstutorial.com:5001/</a><br>
11. <a href="http://hackage.haskell.org/trac/ghc/ticket/2533" target="_blank">http://hackage.haskell.org/trac/ghc/ticket/2533</a><br>
12. <a href="http://article.gmane.org/gmane.comp.lang.haskell.general/16420" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.general/16420</a><br>
13. <a href="http://www.haskell.org/haskellwiki/The_Monad.Reader" target="_blank">http://www.haskell.org/haskellwiki/The_Monad.Reader</a><br>
14. <a href="http://article.gmane.org/gmane.comp.lang.haskell.general/16419" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.general/16419</a><br>
15. <a href="http://thread.gmane.org/gmane.comp.lang.haskell.cafe/44259" target="_blank">http://thread.gmane.org/gmane.comp.lang.haskell.cafe/44259</a><br>
16. <a href="http://thread.gmane.org/gmane.comp.lang.haskell.cafe/44450" target="_blank">http://thread.gmane.org/gmane.comp.lang.haskell.cafe/44450</a><br>
17. <a href="http://article.gmane.org/gmane.comp.lang.haskell.cafe/44211" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.cafe/44211</a><br>
18. <a href="http://www.gamr7.com/" target="_blank">http://www.gamr7.com/</a><br>
19. <a href="http://article.gmane.org/gmane.comp.lang.haskell.general/16422" target="_blank">http://article.gmane.org/gmane.comp.lang.haskell.general/16422</a><br>
20. <a href="http://www.credit-suisse.com/" target="_blank">http://www.credit-suisse.com/</a><br>
21. <a href="http://planet.haskell.org/" target="_blank">http://planet.haskell.org/</a><br>
22. <a href="http://haskell.org/haskellwiki/Blog_articles" target="_blank">http://haskell.org/haskellwiki/Blog_articles</a><br>
23. <a href="http://logicaltypes.blogspot.com/2008/09/what-is-declarative-programming.html" target="_blank">http://logicaltypes.blogspot.com/2008/09/what-is-declarative-programming.html</a><br>
24. <a href="http://changelog.complete.org/posts/752-New-Twitter-Client-Twidge.html" target="_blank">http://changelog.complete.org/posts/752-New-Twitter-Client-Twidge.html</a><br>
25. <a href="http://blog.plover.com/prog/springschool95.html" target="_blank">http://blog.plover.com/prog/springschool95.html</a><br>
26. <a href="http://koweycode.blogspot.com/2008/09/darcs-weekly-news-3.html" target="_blank">http://koweycode.blogspot.com/2008/09/darcs-weekly-news-3.html</a><br>
27. <a href="http://blog.malde.org/index.php/2008/09/09/the-fastq-file-format-for-sequences/" target="_blank">http://blog.malde.org/index.php/2008/09/09/the-fastq-file-format-for-sequences/</a><br>
28. <a href="http://sandersn.com/blog/index.php?title=real_world_haskell" target="_blank">http://sandersn.com/blog/index.php?title=real_world_haskell</a><br>
29. <a href="http://vezzosi.blogspot.com/2008/09/even-if-this-blog-has-been-silent-since.html" target="_blank">http://vezzosi.blogspot.com/2008/09/even-if-this-blog-has-been-silent-since.html</a><br>
30. <a href="http://hackage.haskell.org/trac/hackage/wiki/HBuild" target="_blank">http://hackage.haskell.org/trac/hackage/wiki/HBuild</a><br>
31. <a href="http://rickyclarkson.blogspot.com/2008/09/irc-bot-in-haskell-20-code-80-grr.html" target="_blank">http://rickyclarkson.blogspot.com/2008/09/irc-bot-in-haskell-20-code-80-grr.html</a><br>
32. <a href="http://loupgaroublond.blogspot.com/2008/09/xmonad-08-released.html" target="_blank">http://loupgaroublond.blogspot.com/2008/09/xmonad-08-released.html</a><br>
33. <a href="http://luqui.org/blog/archives/2008/09/07/the-problem-with-coq/" target="_blank">http://luqui.org/blog/archives/2008/09/07/the-problem-with-coq/</a><br>
34. <a href="http://www.jcowie.co.uk/2008/09/haskell-yes-no/" target="_blank">http://www.jcowie.co.uk/2008/09/haskell-yes-no/</a><br>
35. <a href="http://www.haskell.org/mailman/listinfo/haskell" target="_blank">http://www.haskell.org/mailman/listinfo/haskell</a><br>
36. <a href="http://sequence.complete.org/" target="_blank">http://sequence.complete.org/</a><br>
37. <a href="http://planet.haskell.org/" target="_blank">http://planet.haskell.org/</a><br>
38. <a href="http://sequence.complete.org/node/feed" target="_blank">http://sequence.complete.org/node/feed</a><br>
39. <a href="http://haskell.org/" target="_blank">http://haskell.org/</a><br>
40. <a href="http://haskell.org/haskellwiki/HWN" target="_blank">http://haskell.org/haskellwiki/HWN</a><br>
41. <a href="http://code.haskell.org/%7Ebyorgey/code/hwn/" target="_blank">http://code.haskell.org/~byorgey/code/hwn/</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br><br clear="all"><br>
</div>