I posted the following to an internal Microsoft TLA+ group, and I thought it would be worth posting here as well. It in response to a question that provoked a number of other responses which I felt did not adequately address the essence of the question.
You originally wrote:
An action is a formula. It makes no sense to say that a formula has immediate effect. Does the formula 2+3=5 have immediate effect? That no one else has pointed this out shows that many people don’t appreciate the distinction between math and reality.
I have a digital clock on my desk. If I cover part of the display, the clock behaves as follows. It shows a pattern of light and dark regions. For about an hour, that pattern remains quite stable, with barely perceptible changes in light intensity. Then, for a fraction of a second, the pattern fluctuates wildly. It then reaches a different stable pattern. About an hour later, there is another brief period of wild fluctuation followed by another stable pattern. And so on. My brain has learned to recognize the stable patterns as numbers and to ignore the brief fluctuations. When I call the device on my desk a digital clock, I mean that I can think of it as showing the number 22 for about an hour, then the number 23 for about an hour, then the number 0, etc. This allows me to describe a behavior of the clock as a sequence of states---for example, a sequence starting with a state having x=22, followed by a state having x=23, etc. I can describe the set of all such state sequences by a TLA+ formula.
That same TLA+ formula can be interpreted to describe other things. For example, I called the elements of the sequence “states”. I could just as well have called them “events” and have interpreted the sequence as describing a system that releases a sequence of hot air balloons with numbers painted on them. The “event” with x=22 describes the release of a balloon with the number 22 on it. I could also interpret the state sequence as describing a clock falling into a black hole in an imaginary universe, where the clock speeds up as it falls, displaying an infinite sequence of numbers in the few seconds that it takes to reach the event horizon (from the point of view of an external observer). These are perfectly valid interpretations of the behaviors described by the TLA+ formula that I use to describe my clock. However, they are perfectly irrelevant to my clock specification. For that specification, the only important question is: does it provide a useful description of my clock? And the answer to that question depends on what I want to use the description for. It is useful only for applications in which the fact that the states change about once per hour is unimportant. (As I believe someone has pointed out, if that fact is important, we can describe the behavior of the clock as a sequence of states in which the state describes the current time as well as the number currently displayed by the clock.)
The idea that the execution of a sequential algorithm can be described as a sequence of states seems to be due to Turing. It is so widely accepted that most engineers are happy to describe sequential algorithms this way, and to describe my clock in the same way when appropriate. I think the idea that the execution of a concurrent algorithm (or a concurrent system) can also be described by a sequence of states was implicit in the first paper on concurrent algorithms: Dijkstra’s seminal 1965 paper on mutual exclusion. That idea is not widely known, and many engineers need to be shown how to describe concurrent systems in that way. When they learn how to write such descriptions in TLA+, they find them quite useful.
When people get used to describing systems mathematically in a certain way, they tend to confuse the mathematical description with the system. This makes it difficult for them to explain what they are doing to people not familiar with their way of describing systems.
Cheers,
Leslie