Automatically Proving That Computer Programs Do What They are Supposed to Do

Minutes

Corresponding Secretary Robin Taylor called the 2,382nd meeting of the Society to order at 8:01 p.m. Secretary Taylor announced the order of business, announced the evening’s lecture would be livestreamed on the internet, and welcomed new members. The minutes of the previous meeting were read and approved.

President Larry Millstein then introduced the speaker for the evening, Byron Cook, Senior Principal at Amazon Web Services and Professor of Computer Science at University College London. His lecture was titled, “Automatically Proving That Computer Programs Do What They Are Supposed To Do.”

Dr. Cook began with an overview of mathematical proofs. Proving something in math is using logic to be certain that a system works. Because proofing uses the tools of logical analysis, it can be applied to systems of all types.

To prove something mathematically, he said, takes two steps: first, developing the argument, and second, double-checking the argument. From thousands of years ago until very recently, this work was done by human hands. But where it used to be necessary to find a smart person to prove that a theorem holds, around 2001, computer scientists started writing software to take the place of the smart person. Thus the techniques of mathematical proofs can be used in an almost limitless number of contexts. Dr. Cook, for example, has used software to apply mathematical proof techniques to microprocessors, aircraft software, device drivers, and to biological models such as leukemia and diabetes.

But, Cook said, there may be limitations to what computers can do. For example, he said, new students of computer science are invariably introduced to the halting problem. Posed by Alan Turing in the early 20th century, the halting problem asks – whether there exists a system that definitively answers whether there exists an infinite loop in any other system. In modern parlance, can you write a program that will predict whether a Windows program will produce an hourglass symbol, or whether an Apple program will show the user a beachball that never stops spinning?

Dr. Cook then described a halting problem proof in computer code. The program code asks, “if the program halts, then don’t halt,” and “if the program doesn’t halt, then exit – or don’t halt.” Dr. Cook said the program presents the same kind of problem as the statement, “I am a liar,” and cannot be solved.

But though computer scientists have not solved the halting problem, there remains tremendous commercial application in attempting to identify whether a system contains an infinite loop. For example, Cook says one way to think about cancer is as a termination bug in the regular pathways in cells. As another example, the event handling routine of a computer’s mouse device driver should always terminate. When a user moves the mouse, the computer code handling that movement should always do something and then return control back to the computer. Otherwise the computer will hang.

Traditional, pre-digital computer methods of proving termination are difficult in practice and in some cases, impossible in theory. These methods frustrated computer scientists in the pre-digital computer age.

But, when computer scientists revisited the problem with the power of digital computing, they realized they did not always need to prove termination in every instance for there to be a commercial benefit. To illustrate his point, Cook posited that people fly commercial airlines, even though they are not 100% safe, because the occurrence of crashes is so low that people are comfortable with their chances. So, Cook has sought to create rough digital facsimiles of certain systems that solve for halting, and that produce reasonably reliable, but not perfect, results.

Dr. Cook then described the logic and code for some of his work on device drivers, showing an example of how he used proofs to identify a termination problem in computer code. As he mentioned before, that logic is transferable. For example, he has worked with leukemia researchers to answer the question, “when a system is perturbed, does it always go back to a stable state?”

In sum, Dr. Cook said computer scientists first realized around 100 years ago that ancient methods of reasoning could be used to analyze modern industrial artifacts. Then, around 50 years ago, computer scientists became disillusioned when they realized the limitations of these methods. But now, due to the pressures of the commercial marketplace, computer scientists have realized that they do not need to academically identify universal truths. Rather, they can begin by working in the field to make tools that perform adequately in niche areas, which can then be generalized and modified for application in other areas.

Secretary Taylor then invited questions from the audience.

One member asked whether Dr. Cook’s techniques could be used to identify errors in the human brain. Perhaps, Cook responded. His techniques rely on accurate models, so their application to the human brain would be limited by the accuracy of the brain model.

Another member asked whether it was possible to write a program that could identify and repair its own errors. Dr. Cook answered that this question was an area of active research, essentially requiring programs sophisticated enough to search and identify the correct series of inductive questions to identify termination.

A livestream viewer from California asked whether Dr. Cook had applied his techniques to approximations. Yes, Cook said. Representing a very complicated program in a small, finite space can be done by adding nondeterminative variables to the program. Proving the correctness of the program when he has added those variables, logically means that the correctness of the more complicated original program has also been proven.

After the question and answer period, Secretary Taylor thanked the speaker, made the usual housekeeping announcements, and invited guests to join the Society. At 9:21 p.m., Secretary Taylor adjourned the 2382nd meeting of the Society to the social hour.

Attendance: 85
The weather: Overcast
The temperature: 20°C
Respectfully submitted,

James Heelan
Recording Secretary