Leslie Lamport at USI

Leslie Lamport visited the University of Lugano on 11 - 13 of May and gave 3 talks. His main idea is to use math in programming. Before writing a code programmer should try to represent the idea of a program mathematically. This is needed

• to understand better, what he / she is going to implement;
• to formulate the idea precisely without any natural language;
• to avoid bugs before implementing the code.

Lamport did not talk about proving the correctness of programs, but showed on several examples that it is possible to "assign meanings to programs" (see the paper by R.W. Floyd), i.e. mathematical meaning.
Obviously, it is impossible to convince everybody from programmers to CEO that it worth spending time on that (for the same reasons which Fowler mentioned in his "Refactoring"). Therefore this "math" idea can be treated as a long-term message to the software engineering community. Lamport proposes to start from university education and make an emphasis more on math than on programming skills. As soon as a new generation with such an education appears, it will not be difficult any more to convince anybody to use math in programming.
Lamport talked about TLA+ language, which is again a formal math (+ couple of temporal logic operators and some others like ') and about its application for writing specifications. He also presented PlusCal algorithm language, which is based on TLA+, and encouraged to use it in writing algorithms instead of pseudo-code because of PlusCal preciseness. His book on all this stuff is available.

P.S. This text is my own understanding of what was presented and can be different from Lamport's point of view.