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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
