• 
• 

 1 of 2

Gallery

The future according to Microsoft

Posted on 4 Jan 2013 at 14:07

Blue skies to stop blue screens

The work happening at Cambridge isn’t only about hardware. Researcher Georges Gonthier is “even more famous”, says Woodberry, after proving the Feit-Thompson theorem – which states that in “mathematical group theory, every finite group of odd order is solvable”.

That may make little sense to those of us who barely scraped an A-level in maths, but Gonthier’s proof of the idea took six years to solve and two books to publish. “The kind of techniques he had to use to prove that theorem may have applications in areas such as proving software is correct,” explains Woodberry. “It’s a good example of a blue sky thing that’s in Microsoft’s interest to fund, because the chances are it will have a positive impact on things that will affect the company.”

If that sounds far-fetched, consider the last famous mathematical quandary that Gonthier solved: the four-colour theorem. “If you have a map, how many colours do you need to colour every area on the map so that no two adjacent areas are the same colour?” asks Woodberry. “If you think about it, it looks like the answer is probably four – and it is four – but nobody had proven it since 1850 or whatever, and Georges did prove it.”

To achieve this, he used a combination of pencil-and-paper work and computers – and using computers to prove the theorem hadn’t been done before to the satisfaction of mathematicians. “However, the technique that he uses to do the computer-based side of the proof... has been used in something Microsoft built called the ‘static driver verifier’, which we give to third-party partners that are writing driver software for whatever they’re going to attach to the PC, to make those drivers less likely to cause blue screens,” Woodberry explains. “In the old days, when PCs blue-screened more often, it was almost always a driver that caused it. And that software we hadn’t written – somebody else had – and it was usually that software that caused the problem.”

The verifier, based on Gonthier’s work, lets third-party coders check their work – and, as a result, means users see fewer blue screens. “If you said to someone, would it be in Microsoft’s interest to pay somebody whose goal it is to prove the four-colour theorem, they’d probably say no, but in fact it was. In a nutshell, that’s why this model of a bottom-up, researcher-driven blue sky lab really does pay off.”

Searching for better search

The “ten blue links” design of search engines hasn’t changed much since browsers first arrived

Other projects have clear product applications. Woodberry says a lot of “exciting” work is happening around search – clearly to help give Bing a boost over rival Google. However, it isn’t only about technology and algorithms. “Social scientists – sociologists, psychologists, designers – are trying to unpick what people are doing when they go to a web browser,” he says, noting that the “ten blue links” design of search engines hasn’t changed much since they first arrived.

Researchers are looking at why that is, and whether different methods might improve certain types of search tasks. “People have been asking this question for a long time,” he notes.

While Google and Bing both try to deliver the fastest search results possible, that might not be the only way. “Maybe the idea of slow search, rather than instant, [where] you have a long-term interest in something,” he suggests.

Author: Nicole Kobie