On March 14, 2006, Leslie Lamport gave a wonderful guest lecture to undergraduate students at the University of Lugano's Faculty of Informatics. This page contains what little I managed to commit to paper then, as well as my impressions and my totally subjective recollection of events.
Table of Contents
Content
Abstract
Leslie Lamport's Thinking for Programmers was a talk that advocated an approach to software development, based on mathematics, that results in solutions that are succinct, intelligible, and correct.
Complexity
Hardware doubles in complexity every two years; software, on the other hand, doubles in complexity roughly every three years. One way to avert this fate is to rein the sprawl in at the very earliest stage by thinking hard about what we really want and writing it down before we start coding.
Writing
Writing is nature's way of letting you know how sloppy your thinking is; writing down what we want our software to do helps us refine our understanding of it.
The Trouble with Writing
Unfortunately, an informal specification of what a piece of software should do is often not enough to dispel all ambiguities; that requires math. Consider, for example, the description of delete() that one finds in the Java documentation: what should the function do when the file does not exist? Avoiding this kind of trouble requires the conscientious application of mathematical rigor to the specification stage of software development.
Math
Math is nature's way of letting you know how sloppy your writing is; mathematical rigor has proved a solid foundation for other engineering disciplines — why not ours? This notion was first advanced by Robert Floyd, whose 1967 book Assigning Meanings to Programs advocated a new way of looking at computer programs: Floyd proposed that programs be construed and expressed as mathematical relationships between an initial state and a final state. Dr. Lamport illustrated this point by describing how he designed and implemented a prettyprinter for TLA+ using mathematical rules, rather than procedural code.
The Trouble with Math
Though that particular exercise was a noteworthy success, math can give one a false sense of comfort, he said: a "mathematical" specification written by someone whose math skills are unequal to the task can lead to confusion. Consider, for example, the complications that arise from misapplying UML in reasoning about a system's design. This is where formal math comes to the rescue.
Formal Math
Formal math is nature's way of letting you know how sloppy your math is; inventing "new kinds of math" that purportedly supercede "static, old math" is an exercise in vanity and ignorance. Indeed, existing math is up to the challenge; we just need to admit to ourselves that we, software engineers, simply don't know enough math yet. Dr. Lamport then went through the iterative refinement of a "mathematical" solution of a graph problem, showing us how, for many problems, "software bugs" are just obvious "math trivia". In closing, Dr. Lamport insisted that we must embrace mathematics, and recommended that we read pages 1 through 84 and chapter 14 of the TLA+ book for ideas on just how.
The Trouble with Formal Math
The trouble with rigorous math is that it's hard work; that, however, turned out to be a topic for another lecture.
Form
The Good
Dr. Lamport spoke audibly and intelligibly. The pace was neither too fast nor too slow, and there were plenty of well-placed micro-pauses for reflection. The base knowledge assumed of students (basic discrete math) was reasonable. Entertaining anecdotes motivated and illustrated points well. He spoke his mind freely concerning various alleged "best-practices" and earned the approbation of the progressive faction of the undergraduates in so doing; his earnestness and his confidence in the value of his approach certainly impressed me. After "finishing" the slides, he answered our questions patiently and generously.
The Bad
I loved every bit of it, but a discussion of the event in the first-year lab revealed that several slides were too “deep” for some of the students.
The Ugly
It seems Dr. Lamport raised some hackles with his candid appraisal of some current “best-practices,” though this probably says more about the offended listeners than about the lecturer. Also, he claimed that many in the current generation of software engineering professionals and educators are ill-prepared to teach mathematics at the level required to help the next generation advance the state of the art in our profession — and that may have bruised some egos, too. So, long-story-short: if you want to shake things up a bit, you should call on Dr. Lamport! :-)
Summary
Lamport impressed me as the rare kind of theoretician who, not content with advancing the state of the art, reaches out to practicing engineers in the hope of raising the standard of so-called best-practices. He seemed genuinely concerned about the challenges faced by software engineering professionals, and demonstrated a patient understanding of the many reasons why the pace of progress is slow. Moreover, he seems to be as fond of young people as he is of mathematics, and casts a resolute vote of confidence in us; I hope that, along with all of the mathematical methods, some of this attitude will rub off on our entire faculty, too! :-)