I’m back in Tampa after my sweet honeymoon with my darling new wife, Linnea. We spent a week in my home town, Washington, DC, where she had never been.
Now back to my task of asking you tough questions and learning from your answers.
Ben Linders interviewed you for InfoQ on the subject of provably correct software on May 22, 2015.
You were articulate and clear. Obviously you have been thinking about the many problems of software engineering that arise from the difficulty of writing bug-free code and producing bug-free products and systems. Since many smart engineers and researchers have been thinking about this for decades, it is remarkable, I think, that we still read of bugs in crucial, widely used software produced by, we suppose, the best engineering talent available.
I’d like to ask you to consider the remarkable bug recently uncovered in some Apple products that became known at about the time your interview appeared.
Here’s a description of the problem. There are many other articles about this bug. I’ll summarize the problem, as I understand it, as follows: Someone sends you a text message with a precise and particular string of characters, including some specific ones in Arabic (!). When you open the message to read it, the system’s attempt to display the character sting crashes the operating system. Indeed, the damage is so great that it is difficult to restore the operating system properly.
Evidently, this afflicts iOS in iPads, iPhone, and Apple Watches. Of course, no one is likely to receive this message, and in that sense, this is not exactly a serious bug. But what other obscure patterns of symbols might do this?
My question to you is whether the methods of formal correctness proofs and other aspects of meta-analysis of code and applications could locate such a bug? Since Apple’s engineers are among the best, why would they have failed to find a bug that can crash their operating system, if solid and effective methods such as those you describe are available?