原创 Why can't we completely eliminate bugs?

I recently had an experience with two awesomely beautiful designs. To my disappointment, I also encountered some bugs, which caused me to wish that formal verification tools had been used as part of the development process.

The Apple of my eye
Last month, I persuaded my family to abandon their Windows machines due to too many bugs -- more bugs than I care to list throughout years of use. We purchased the newly released 27-inch iMac with a 5k Retina display. This is a beautiful computer with a strikingly sharp image powered by 14.7 million pixels, and we were all excited to get our hands on the system.

However, it didn't take long for me to experience the first set of bugs. I needed to use "Migration Assistant" to transfer files from my MacBook Air laptop to the new iMac. This should have been a simple task, but it proved to be much more difficult than it should have been. Here's what transpired:

- I connected my MacBook Air to the iMac using a Thunderbolt cable and did all the steps instructed by Migration Assistant. The iMac didn't see the fast Thunderbolt connection. It was using WiFi to transfer data, and it projected a 76-hour time to do so. After struggling for a while and finding no answer with iMac itself, I resorted to web forums and found the trick: I had to boot my MacBook Air as an external hard disk for the iMac to see the Thunderbolt connection. If this is required, why doesn't Apple provide instructions?

- At first, the migration process seemed to go smoothly. Eventually, the system reported that it would take less than a minute to finish the process. I waited and waited and waited. Nothing changed after 30 minutes, and it seemed like it was stuck. A new web search revealed many angry users who experienced the same problem as early as the beginning of the year. Many lost all their migration work after waiting hours. Talk about the anger and frustration. Apparently, this is caused by a few incompatible files, and it raises a simple question: Why doesn't Apple provide the information up front instead of waiting until the end of the process?

- Just as I was about to kill my process, the computer informed me about the incompatible files. The migration process gave every indication of having completed -- but not yet. A key motivation for buying the iMac was to move all my photos and videos to this beautiful machine. When I checked on the results, however, those files had not migrated. I'm not sure why. I ended up doing a manual copy of files between the two machines. It was past midnight by then, and I had been doing this for more than four hours. Frustrated and tired, I almost wanted to give up on the new machine and return it to Apple.

Apple is well known for its ease of use, yet it couldn't get this right. Data migration is one of the first things a user might be expected to do after buying a new machine, so why was my experience so difficult and frustrating? What makes this even more frustrating is the fact that users reported all these issues months ago, yet there are still bugs with the recent release of the O/S X Yosemite operating system.

Come fly with me
I traveled to Shanghai on Air Canada through Vancouver in early November. Much to my pleasant surprise, Air Canada has started using Boeing 787 Dreamliners on this route. The aircraft is brand new and beautiful. The interior is roomy and comfortable. At first glance, everything appeared to be wonderful.

Unfortunately, it didn't take long before some bugs started to appear.

- As we were about to take off, our captain reported that there was a mechanical issue with the aircraft, and we needed to wait for the repair crew to fix it. No detailed explanation was given about the issue. Luckily, the airplane managed to depart 25 minutes later. Presumably, the issue was fixed.

- The Boeing 787 has many new and improved features, including an electrochromic dimmable system intended to be an improvement to traditional window shades. Users can control how much light passes through the window by changing the tint of the glass. This seems to be a nice feature, though I soon discovered that its designer(s) hadn't thought through all the possibilities. The darkest window setting will still allow plenty of light to come through, especially if the sun itself is right outside the window. Throughout the flight from Vancouver to Shanghai, we were chasing the sun, resulting in a big, bright glare through the window. When we complained about it, the flight attendant taped a piece of paper to the window. It is ironic that such a new, "improved" feature turned out to be so flawed. I wonder how long it will take for Air Canada to put the original window shades back. They may not be fancy, but they work.

- Halfway through the flight, the in-flight entertainment system began to have issues. After several attempts to reset it, the captain reported that the problem couldn't be solved.

It makes me wonder
Why do great designs like those mentioned here still have bugs? There could be any number of reasons, but I think one problem is that the engineers who design and test systems cannot think about all possible test scenarios. The tools used for testing depend on humans to come up with test scenarios, but the limitations of the human brain mean the results of the testing will not be complete.

This makes me appreciate the beauty of formal verification. It removes the requirement for designers and verification engineers to come up with all the possible scenarios that need to be tested. By automatically enumerating the entire search space, corner cases that humans may not consider can still be tested. If formal technology could be used for system or software testing, maybe there would be no bugs left in our world.

There is still a long way to go to reach this goal, but semiconductor companies large and small are embracing formal technology for chip design and verification at record speed. Maybe, just maybe, we can dream about a day in the not-so-distant future when systems don't just look good, but also work beautifully without any glitches.

Jin Zhang is senior director of marketing at Oski Technology.