Email Gateway (Aug 22 2022 at 09:45): Email Gateway (Aug 22 2022 at 09:45):From: "W. Douglas Maurer" <maurer@gwu.edu>
This well-known cartoon proves that the words "bug" and "feature" are
meaningless.
Makarius - You've been saying for a long time that "bug" is
meaningless, but the other contributors to the Isabelle/Isar
Reference Manual don't seem to agree with you. Searching that manual,
I find 15 uses of the word "debugging" in that manual.
Personally I prefer "bug" to "error" (which is what "bug" means, at
least in the US) because "error" sounds more serious, more like an
erroneous way of thinking that would require a major rewrite to fix,
whereas a "bug" is more typically either a typographical error or
something similar, that can be repaired in either one line or a very
few lines.
If "bug" means something different where you live, please advise.
Thanks! -WDMaurer
Last updated: Nov 21 2024 at 12:39 UTC