IFIP WG2.2 40th Anniversary Meeting (4): SOS
I mentioned that the main interest of the meeting for me was the clash of cultures exhibited in the talks of Lamport and Plotkin. I haven't spoken much about the second.
Plotkin spoke about the history of Structur(al/ed) Operational Semantics. There is a paper about it, written with somewhat more caution than the talk
(Gordon D. Plotkin. The origins of structural operational semantics. Journal
of Functional and Logic Programming, 2003).
Plotkin clearly believes that SOS is a very simple way of giving meaning to programs; he speaks of "symbol pushing" and the fact that SOS doesn't require mathematics to understand, and the fact that unnecessary detail of implentation is hidden. This is in sharp distinction to Lamport who cites always mathematics as the solution to problems, and insists that state involved in the implementation should not be hidden.
My view is
(i) that the symbol pushing nature of SOS is one small aspect of computing - inflated to seem the whole;
(ii) the fact that denotational semantics has been superceded by this primitive operational semantics is due to the inadequacies of a development centred on higher-order aspects;
(iii) programmers don't really think that manipulating program text is the content of programming;
(iv) the fact that programming text becomes state, instead of representing a sequence of actions between states, arises also in part because of the confusion between general purpose machines and the particular machine defined by any program;
(v) SOS has in principle nothing to do with compositionality.
The theory of computers should separate issues that are fundamentally different rather than choosing one aspect and trying to fit everything into this corner.
Plotkin spoke about the history of Structur(al/ed) Operational Semantics. There is a paper about it, written with somewhat more caution than the talk
(Gordon D. Plotkin. The origins of structural operational semantics. Journal
of Functional and Logic Programming, 2003).
Plotkin clearly believes that SOS is a very simple way of giving meaning to programs; he speaks of "symbol pushing" and the fact that SOS doesn't require mathematics to understand, and the fact that unnecessary detail of implentation is hidden. This is in sharp distinction to Lamport who cites always mathematics as the solution to problems, and insists that state involved in the implementation should not be hidden.
My view is
(i) that the symbol pushing nature of SOS is one small aspect of computing - inflated to seem the whole;
(ii) the fact that denotational semantics has been superceded by this primitive operational semantics is due to the inadequacies of a development centred on higher-order aspects;
(iii) programmers don't really think that manipulating program text is the content of programming;
(iv) the fact that programming text becomes state, instead of representing a sequence of actions between states, arises also in part because of the confusion between general purpose machines and the particular machine defined by any program;
(v) SOS has in principle nothing to do with compositionality.
The theory of computers should separate issues that are fundamentally different rather than choosing one aspect and trying to fit everything into this corner.
Labels: computing