Interesting Read (fwd)

[Frank Atanassow]

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