As a side note, I do enjoy Overcoming Software and your presentations (including and maybe especially the stuff about error handling).
Thank you for sharing your knowledge!
I think I must have rubbed you the wrong way for some reason. Here are my short answers.
Type Safety: I have been trying to think deeply about what could have prevented any of the escaped bugs I encounter.
In my accounting, way over half could been prevented by stronger types. Sure, anything can be overdone, e.g. I can add safety in places which are not error prone just adding cost to future refactoring. Anything in programming can be misused.
About the quality of error outputs: I wrote about it in my other posts complaining about Maybe overuse where error information exists and is suppressed, about alternative use that will throw troubleshooters for a loop. E.g. Alternative is implemented in IO by swallowing error information:
mplusIO :: IO a -> IO a -> IO a
mplusIO m n = m `catchException` \ (_ :: IOError) -> n
the end result is code where error output is something that is hard to trust. I am not saying people are forced to overuse these concepts, I am saying that I am observing the overuse in the code I work on.
I am not claiming that good error outputs are trivial, I am saying that in my experience the error output quality is lower in FP programs. That judgement may not resonate with some readers, e.g. someone could compare Haskell to an (often not existent) error handling in JS.
About mathematicians and errors. Let me quote part of what I wrote:
“This is kinda fun to think about: we have only empirical evidence of mathematics itself being correct, we know we will never prove it formally. Mistakes in mathematics are extremely rare. However, we have a lot of empirical evidence of (past) incorrectness in various empirical sciences. I am a pragmatist enough to say that mathematics is correct, the rest looks good only until we learn more about it (just like bugs in software)”
We are talking about empirical observability here. I have not experienced many invalid proofs in my career. Granted, I did not stay in that field for long only a few years. I was an editor for a mathematical publication as part of my duties for maybe 2 years and have reviewed a few papers before they had been published. I have obviously read many and wrote quite a few and my experience matches Alice’s.
Can you provide examples? Oh yes, you probably will give me some well known case like the original Wiles’ proof of Fermat’s theorem. Do you know about any statistics which shows some significant, say 0.1% error rate in math proofs? I do not. I do know about some quite high statistics of, e.g. misdiagnosis in medical fields, error rates in software, etc.
A cool example is to compare Turing’ and Church’ work on undecidabilty, Turing machines had initial bugs, LC paper (as far as I know) did not. But this is obviously only one example.
Repeating myself, the argument is observational, I put incorrect proofs under “exceptions that prove the rule” of these being very rare. They are rare and thus we talk about them when they happen. To me formal is the essence of correctness.
The bits you pointed out are a small sample of topics considered in my article.
My main goal was to talk about different mindsets in the context of improving communication and understanding these mindsets. To do that I had to exaggerate a little and present these in a binary, stereotypical way.
I was sorry to learn that you found nothing positive to say about my article.
