I can't make much sense of Djikstra's linguistic points either. But with the little I can understand, my objection boils down to the following statement:
> A programming language, with its formal syntax and with the proof rules that define its semantics, is a formal system for which program execution provides only a model. It is well-known that formal systems should be dealt with in their own right, and not in terms of a specific model. And, again, the corollary is that we should reason about programs without even mentioning their possible "behaviours".
Perhaps this is another aspect of the "SWE vs. CS" debate but I've come to the conclusion that in SWE, it makes more sense to reason about entities and how they behave (deliberate use of the word) rather than in terms of every single line of code. Said another way, anthropomorphizing programs is another means of abstraction and SWEs and CSs alike should be comfortable going up and down the abstraction ladder as needed. Even in academia, outside your first two programming classes or so, outside algorithms, it is rare to spend time in the realm of "formal syntax and proof rules". (Or maybe this is simply a difference of the needs of CS education today and during Djikstra's time.)
But why should we encourage reasoning in this manner? I have many reasons but the bluntest (yet holds no less water) one is because I think Djikstra's statement assumes you have access to the readable source code. That's simply not true. So it's more useful to reason about computing units as entities with "behaviors".
In the real world, (outside of compiler development) we rarely discover arbitrary code without context. Usually, we are writing that code to fulfill some business purpose. Without being able to describe the behavior of the system, we'd never be able to design any practical software that exists outside of pure math.
> A programming language, with its formal syntax and with the proof rules that define its semantics, is a formal system for which program execution provides only a model. It is well-known that formal systems should be dealt with in their own right, and not in terms of a specific model. And, again, the corollary is that we should reason about programs without even mentioning their possible "behaviours".
Perhaps this is another aspect of the "SWE vs. CS" debate but I've come to the conclusion that in SWE, it makes more sense to reason about entities and how they behave (deliberate use of the word) rather than in terms of every single line of code. Said another way, anthropomorphizing programs is another means of abstraction and SWEs and CSs alike should be comfortable going up and down the abstraction ladder as needed. Even in academia, outside your first two programming classes or so, outside algorithms, it is rare to spend time in the realm of "formal syntax and proof rules". (Or maybe this is simply a difference of the needs of CS education today and during Djikstra's time.)
But why should we encourage reasoning in this manner? I have many reasons but the bluntest (yet holds no less water) one is because I think Djikstra's statement assumes you have access to the readable source code. That's simply not true. So it's more useful to reason about computing units as entities with "behaviors".