Edsger W. Dijkstra, one of 20th century's famous computer programmers, posed the following mathematical question in February 1981:

• "Given a specific function, called lambo, how do you prove that it is equal to its own inverse?"

Along with several similar ones, this question illustrates Dijkstra's active involvement with mathematical methodology during the 1980s and 1990s.

Dijkstra proved the above result by writing an original computer program that calculates lambo and by gradually transforming that into a symmetric program --- a program that is useless to the programmer but of value to the mathematician! In contrast to the practical programs that he had written for real, finite, computing machines during the 1950s, he was now writing non-terminating programs in which variables obtain arbitrarily large values and where function values are calculated ad infinitum.

Dijkstra's proof furthermore demonstrates how he transferred what programming methodology had taught him to mathematical methodology: symmetry, so dear to him in his earlier years as a programmer, also played a crucial role in his mathematical methodology and in his lambo example.

Calculational reasoning became Dijkstra's main occupation in the second half of his career. Instead of viewing a program text as an operational description of an abstract machine as he had done during the 1960s, and instead of making analogies to sharpen his intuitive understanding of the problem at hand, Dijkstra began to view a program text as a formula, representing a predicate, in a formal system.

The contradistinction between the younger Dijkstra, the programmer, and the older Dijkstra, the mathematician, is the main theme of my presentation. I will paint a picture of how Dijkstra projected ideas from mathematics onto programming in the 1960s and 1970s, before describing the projection in the other direction --- from programming methodology to mathematical methodology --- and before zooming in on the specific lambo example.