Here are two things I found interesting: 1. The author comments that programs are not theorems. He is correct. They are, instead, proofs of theorems. The problem is, programmers almost never know what theorems their programs prove. 2. All of the criteria the authors gives for "good languages" apply, in spades, to Haskell, except the point on libraries. On that one, we're pedaling as fast as we can, but there aren't enough of us. Rex Page ---------- Forwarded message ---------- Date: Tue, 18 Feb 2003 20:22:46 -0800 (PST) From: David Sankel <camio@yahoo.com> To: Haskell Mailing List <haskell@haskell.org> Subject: Interesting Read An interesting read: http://www.paulgraham.com/popular.html Any thoughts? ---- David J. Sankel _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
hi, Rex Page wrote:
... 1. The author comments that programs are not theorems. He is correct. They are, instead, proofs of theorems. The problem is, programmers almost never know what theorems their programs prove. ... my programs always prove IO(). this must be the best proven theorem in Haskell. and people just keep on proving it :-)
bye iavor -- ================================================== | Iavor S. Diatchki, Ph.D. student | | Department of Computer Science and Engineering | | School of OGI at OHSU | | http://www.cse.ogi.edu/~diatchki | ==================================================
Iavor S. Diatchki wrote:
my programs always prove IO(). this must be the best proven theorem in Haskell. and people just keep on proving it :-)
I believe that I have proven more often that undef = undef and my students prove usually that GHC typechecker is a nasty, unforgiving beast. Jerzy Karczmarczuk (of course this posting belongs rather to the list haskell-beer ...)
G'day. On Wed, Feb 19, 2003 at 09:46:02AM -0600, Rex Page wrote:
Here are two things I found interesting: 1. The author comments that programs are not theorems.
No, he argues that programming _languages_ are not theorems. All that is required of a theorem is that it is correct. A tool, on the other hand, not only has to work (i.e. it has to correctly accomplish some task), it also has to be safe to use, its controls must be meaningful to the intended user, it should be in some way better than the tool which it replaces and so on. Cheers, Andrew Bromage
Andrew J Bromage wrote (on 20-02-03 10:26 +1100):
All that is required of a theorem is that it is correct.
A tool, on the other hand, not only has to work (i.e. it has to correctly accomplish some task), it also has to be safe to use, its controls must be meaningful to the intended user, it should be in some way better than the tool which it replaces and so on.
In practice, one requires more of a theorem than that it simply be correct. One also wants simple, readable and, when possible, multiple inequivalent proofs of the theorem, organized into meaningful lemmas which might be reused to prove other theorems. Conversely, one wants the proof to use the theorems and lemmas of others. Much the same, you will note, holds of programs and program specifications. In addition, some people consider constructive proofs superior to classical proofs, not only for practical (e.g., deriving an algorithm) reasons, but also for pedagogical and philosophical reasons. And these days, the practice of writing executable specifications in, oh, say Haskell, is becoming increasingly popular. Regards, -- Frank
participants (5)
-
Andrew J Bromage -
Frank Atanassow -
Iavor S. Diatchki -
Jerzy Karczmarczuk -
Rex Page