A Heidelberg dialogue: Two laureates sit down to discuss proofs

Andrei Mihai

In an informal dialogue that took place in Heidelberg, laureates Whitfield Diffie and Leslie Lamport sat down with Tom Geller to discuss good proofs, bad proofs, and why we should care about it.

Diffie, known for being one of the pioneers of public-key cryptography, started off by saying that he often thinks about himself as a mathematician, not a computer scientist.

“Both of us, in effect, are in a group of people who’s declining – we thought of ourselves as mathematicians who came to computer science.”

The difference may seem trivial, but it can be meaningful especially when it comes to how you think about problems – and proofs. In particular, mathematicians tend to be stricter and more careful with the way they deal with proofs and bugs in algorithms.

“A programmer can ignore some things that a scientist wouldn’t, and a mathematician wouldn’t,” Lamport concurs. Lamport is likely familiar to the young researchers as the creator of LaTeX — a widely used software system for document preparation. But Lamport is also the creator of TLA+ a formal specification language that can be described as exhaustively testable pseudocode.

TLA+ itself clearly shows how important proofs are to Lamport. It’s not a programming language – instead, it’s based on mathematics and logic, with specifications written with precise, formal language. In fact, TLA+ itself is sometimes used to write machine-checked proofs of correctness both for algorithms and mathematical theorems. The proofs are written in a hierarchical style.

According to Lamport, mathematicians are sometimes surprisingly bad at writing proofs (and presumably, engineers or programmers are even worse). In anecdotal observations, he found that 1 in 3 mathematical proofs contain an incorrect theorem. When this happens, it can lead to real-life problems.

“Something that appeared in the past few years that disturbed me very much,” said Diffie. “There a protocol called WPA2 used in wifi, and it was proven correct, and yet it was broken. What that means is that they’ve proved the wrong theorem — in short, they have not drawn the right specification for what they want. In fact, the way in which it was broken is something known.”

There are at least two major vulnerabilities with WPA2 (which is a standard used to secure the vast majority of Wi-Fi networks). In 2016, it was shown that the WPA2 contains an insecure expository random number generator. If the generator is used, attackers can predict the group key that is supposed to be random. Furthermore, in 2017, the so-called KRACK attack showed how an attacker can gradually match encrypted packets to fit the keychain used in encryption. This is not related to how the standard is implemented, but rather the standard itself. Despite patching attempts, this vulnerability still remains problematic. Bugs always happen in programming but making a proof error can be damning.

Proofs need to be extremely rigorous. Lamport recalls a famous internet “proof” that all triangles are isosceles. Obviously, this cannot be true, but reading the “proof” can make you question all the geometry proofs you wrote in highschool. Furthermore, proving something isn’t always straightforward, and it doesn’t always lead to understanding things.

“I succeeded in proving the correctness of an algorithm but I couldn’t still understand it. This is not generally how things work, but it does demonstrate the power of rigorous mathematical thinking, as a supplement to understanding,” Lamport recalls.

However, the two agree that despite some hiccups, programming has grown and developed tremendously. It used to be on the periphery of mathematics, while now it is pretty much embedded in every field of science – something which was also mentioned in a previous dialogue at the #HLF21.

“I thought that what was wrong with programming was that it was solitary, unlike mathematics which really has a lot of wind and cross-discussion, cross-culture, and when people prove a new theorem and present it at a seminar and lots of people listen to it and send it to the journal and the referees work through it,” Diffie says.

The two also have some advice for young researchers, both on what they could focus their energy on, and on how to write proofs.

For instance, when it comes to proving things hierarchically, splitting an algorithm into its parts and proving them individually, it’s often unclear how far down you have to go proving things. At what point is the proof obvious and you should stop?

“My advice is to split it down to the level where you think is absolutely completely obvious, and then go another one-two levels,” Lamport says, much to Diffie’s delight.

The two were also asked if there are any algorithms that resist proofing, and they agreed that two types of algorithms resist proofs: those that are obviously simple, and those that are wrong.

“If you have something so simple everyone agrees it’s obvious, like an axiom or something like that,” Diffie says.

Lamport added: “A lot of programs resist proving because they’re incorrect. But on the other hand, this doesn’t keep some people from proving them.”

The laureates also discussed what machine learning can bring to the field of proofs — and Lamport recommends that young researchers have a look at this field because it’s one that’s about to have a breakthrough soon.

“Machine learning would fit in wonderfully by creating proof by methods that we don’t understand at all, but that’s fine if what they create with it is something that can be checked by a program. To my knowledge, this has not happened yet but it’s clearly going to happen soon and it’s a marvelous field for research – for all you young researchers out there,” he concludes.

The post A Heidelberg dialogue: Two laureates sit down to discuss proofs originally appeared on the HLFF SciLogs blog.