I have a newbie question....  Does theorem proofs have a use for an application?  Take for example the IRC bot example (http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot)  listed below.  Is there any insight to be gained by theorem proofs (as in COQ) into the app? 

Thanks,

Daryoush

On Sat, Sep 13, 2008 at 4:07 PM, Brent Yorgey <byorgey@seas.upenn.edu> wrote:
---------------------------------------------------------------------------
Haskell Weekly News
http://sequence.complete.org/hwn/20080913
Issue 85 - September 13, 2008
---------------------------------------------------------------------------

  Welcome to issue 85 of HWN, a newsletter covering developments in the
  [1]Haskell community.

Announcements

  citeproc-hs. Andrea Rossato [2]announced the first release of
  [3]citeproc-hs, a Haskell implementation of the [4]Citation Style
  Language. citeproc-hs adds a Bibtex-like citation and bibliographic
  formatting and generation facility to [5]Pandoc.

  Twidge. John Goerzen [6]announced the release of [7]Twidge, a
  command-line Twitter and Identi.ca client.

  Real World HAppS: Cabalized, Self-Demoing HAppS Tutorial (Version 3).
  Thomas Hartman [8]announced a new version of [9]happs-tutorial, with a
  correspondingly updated [10]online demo.

  generic list functions fixed. Jim Apple reported that genericTake,
  genericDrop, and genericSplitAt have [11]been fixed so they are now
  total functions (they used to fail on negative integer inputs, unlike
  their ungeneric counterparts).

  The Monad.Reader (13) - Call for copy. Wouter Swierstra [12]announced a
  call for copy for Issue 13 of the [13]Monad.Reader. The deadline for
  submitting articles is February 13, 2009.

  Heads Up: code.haskell.org is upgrading to darcs 2. Duncan Coutts
  [14]announced that /usr/bin/darcs on code.haskell.org will soon be
  upgraded to version 2. Most users should be unaffected as darcs 2 works
  just fine with repositories in darcs 1 format, and has been extensively
  tested for correctness.

Discussion

  packages and QuickCheck. Conal Elliott [15]asked what methods of
  organization people use to package up QuickCheck tests for their
  libraries.

  Hackage needs a theme song!. Jason Dagit wrote a [16]theme song for
  Hackage!

Jobs

  Gamr7. Lionel Barret De Nazaris [17]announced that [18]Gamr7, a startup
  in France focused on procedural city generation for the game and
  simulation market, is looking for a senior developer/technical
  director.

  senior role at Credit Suisse. Ganesh Sittampalam [19]announced that
  [20]Credit Suisse is seeking to recruit an expert in functional
  programming for a senior role in the Global Modelling and Analytics
  Group (GMAG) in the Securities Division.

Blog noise

  [21]Haskell news from the [22]blogosphere.
    * Douglas M. Auclair (geophf): [23]What is declarative programming?.
    * John Goerzen (CosmicRay): [24]New Twitter Client: Twidge.
    * Mark Jason Dominus: [25]Return return. Mark's mind is blown by the
      code "return return" appearing in a paper by Mark Jones.
    * Eric Kow (kowey): [26]darcs weekly news #3.
    * Ketil Malde: [27]The FastQ file format for sequences.
    * >>> Nathan Sanders: [28]Real World Haskell. Nathan experiments with
      porting some of his Python code to Haskell.
    * Andrea Vezzosi (Saizan): [29]Results from GSoC. Andrea's GSoC work
      on a high-level dependency framework for Cabal is going to be
      released in a separate package for now, [30]hbuild.
    * >>> Ricky Clarkson: [31]An IRC Bot in Haskell, 20% code, 80% GRR.
      Ricky shares his experiences, frustrations, and eventual success
      writing a simple IRC bot in Haskell.
    * >>> Yaakov Nemoy: [32]Xmonad 0.8 released.
    * Luke Palmer: [33]The problem with Coq. ...is, according to Luke,
      that it doesn't have a nice graphical interface.
    * >>> James Cowie: [34]Haskell! yes no?. James dives into learning
      some Haskell. Verdict so far: a "very nice language".

Quotes of the Week

    * EvilTerran: this is hard to express in this type system. i'm going
      to make my own type system instead!

About the Haskell Weekly News

  New editions are posted to [35]the Haskell mailing list as well as to
  [36]the Haskell Sequence and [37]Planet Haskell. [38]RSS is also
  available, and headlines appear on [39]haskell.org.

  To help create new editions of this newsletter, please see the
  information on [40]how to contribute. Send stories to byorgey at cis
  dot upenn dot edu. The darcs repository is available at darcs get
  [41]http://code.haskell.org/~byorgey/code/hwn/ .

References

  1. http://haskell.org/
  2. http://article.gmane.org/gmane.comp.lang.haskell.cafe/44471
  3. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/citeproc%2Dhs
  4. http://xbiblio.sourceforge.net/csl/
  5. http://johnmacfarlane.net/pandoc/
  6. http://article.gmane.org/gmane.comp.lang.haskell.cafe/44453
  7. http://software.complete.org/twidge
  8. http://article.gmane.org/gmane.comp.lang.haskell.cafe/44410
  9. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/happs-tutorial
 10. http://happstutorial.com:5001/
 11. http://hackage.haskell.org/trac/ghc/ticket/2533
 12. http://article.gmane.org/gmane.comp.lang.haskell.general/16420
 13. http://www.haskell.org/haskellwiki/The_Monad.Reader
 14. http://article.gmane.org/gmane.comp.lang.haskell.general/16419
 15. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/44259
 16. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/44450
 17. http://article.gmane.org/gmane.comp.lang.haskell.cafe/44211
 18. http://www.gamr7.com/
 19. http://article.gmane.org/gmane.comp.lang.haskell.general/16422
 20. http://www.credit-suisse.com/
 21. http://planet.haskell.org/
 22. http://haskell.org/haskellwiki/Blog_articles
 23. http://logicaltypes.blogspot.com/2008/09/what-is-declarative-programming.html
 24. http://changelog.complete.org/posts/752-New-Twitter-Client-Twidge.html
 25. http://blog.plover.com/prog/springschool95.html
 26. http://koweycode.blogspot.com/2008/09/darcs-weekly-news-3.html
 27. http://blog.malde.org/index.php/2008/09/09/the-fastq-file-format-for-sequences/
 28. http://sandersn.com/blog/index.php?title=real_world_haskell
 29. http://vezzosi.blogspot.com/2008/09/even-if-this-blog-has-been-silent-since.html
 30. http://hackage.haskell.org/trac/hackage/wiki/HBuild
 31. http://rickyclarkson.blogspot.com/2008/09/irc-bot-in-haskell-20-code-80-grr.html
 32. http://loupgaroublond.blogspot.com/2008/09/xmonad-08-released.html
 33. http://luqui.org/blog/archives/2008/09/07/the-problem-with-coq/
 34. http://www.jcowie.co.uk/2008/09/haskell-yes-no/
 35. http://www.haskell.org/mailman/listinfo/haskell
 36. http://sequence.complete.org/
 37. http://planet.haskell.org/
 38. http://sequence.complete.org/node/feed
 39. http://haskell.org/
 40. http://haskell.org/haskellwiki/HWN
 41. http://code.haskell.org/~byorgey/code/hwn/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe