Most of the new draft of the Concurrent Programs paper has to do with trying to specify problems and solutions in synchronization via an atomic “compare and swap” operation. Even these operations are surprisingly complicated once put under the microscope – or not so surprisingly complicated if you think about the details of using or implementing them. But at the end of the paper, I start to describe the fundamental difference in approach between this work and “formal methods” in terms of how we can view a program. Dijkstra seems to me to have made an error by insisting that we should think of a program as a mathematical object and a programmer as a mathematician of sorts. A program is more of a manufactured object.
Even though it has no weight and is invisible, a program is device of sorts. If we think of a program as a mathematical object, the methods of formal logic – of meta-mathematics – are the natural methods to use. If we think of a program as a device, like a piano or a bathtub or an automobile, then what mathematicians call “foundational questions” are far away. People are very resistant to the idea of a program as a “thing” for the obvious reasons, but mathematical objects don’t have the weird properties and defects of manufactured objects (or physical objects for that matter). A ball bearing is not a sphere and an implementation of a stack is not an ordered sequence. Recursion in programs is different from recursion in mathematical functions: f(0):=1, f(x+1):= (x+1)*f(x) is a complete definition of a mathematical object but only an approximation of some of the properties of the program written the same way. Any programmer will know that f(10000) almost certainly fails – and that’s an important part of the specification of the program.
The confusion between programs and mathematical objects is a pervasive obstacle in fields as apparently unrelated as program verification, software pricing, and patent law. In program verification we bog down in foundational methods of formal logic because that is the obvious tool to study mathematical objects, but it’s certainly not the obvious tool for doing mathematics or describing manufactured objects. In software pricing, the resistance of manufacturers to let mere software figure in to costs in terms of how complex it is and how much it adds to value rather than by weight repeatedly leads to product development schedules that invest too little time and/or money in the most important components. In patent law, confusion between unpatentable mathematical methods and technology for programs is used to deny software innovators the same rights that are uncontroversially granted to innovators who design cardboard boxes