| Let me also address this with some snarky quotes by Lamport[1] (and just add, that having tried what he suggests on real-world programs, although what he says may sound more complicated, it is actually simple): > Computer scientists collectively suffer from what I call the Whorfian syndrome — the confusion of language with reality > [R]epresenting a program in even the simplest language as a state machine may be impossible for a computer scientist suffering from the Whorfian syndrome. Languages for describing computing devices often do not make explicit all components of the state. For example, simple programming languages provide no way to refer to the call stack, which is an important part of the state. For one afflicted by the Whorfian syndrome, a state component that has no name doesn’t exist. It is impossible to represent a program with procedures as a state machine if all mention of the call stack is forbidden. Whorfian-syndrome induced restrictions that make it impossible to represent a program as a state machine also lead to incompleteness in methods for reasoning about programs. > To describe program X as a state machine, we must introduce a variable to represent the control state—part of the state not described by program variables, so to victims of the Whorfian syndrome it doesn’t exist. Let’s call that variable pc. > Quite a number of formalisms have been proposed for specifying and verifying protocols such as Y. The ones that work in practice essentially describe a protocol as a state machine. Many of these formalisms are said to be mathematical, having words like algebra and calculus in their names. Because a proof that a protocol satisfies a specification is easily turned into a derivation of the protocol from the specification, it should be simple to derive Y from X in any of those formalisms. (A practical formalism will have no trouble handling such a simple example.) But in how many of them can this derivation be performed by substituting for pc in the actual specification of X? The answer is: very, very few. > Despite what those who suffer from the Whorfian syndrome may believe, calling something mathematical does not confer upon it the power and simplicity of ordinary mathematics. Obviously, we all suffer from the Whorfian syndrome, but I think it's worthwhile to try and shake it off. Luckily, doing it doesn't require any study -- just some thinking. [1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/d... |