|
Thanks for a great and insightful article and answer. Views like yours should be shared by a wider audience, since it accentuates a section of software engineering that is rarely discussed: understanding and adjusting the mental model of programming (or should I say: systems design?) Applying formal methods does not automatically entail that a system is proven to be correct, which would be an exaggeration. Proponents of formal methods believe it helps to ascertain certain robustness and reliability aspects of a system. For example, I could prove a Paxos implementation correct, given the specification of a Paxos algorithm, but still use it incorrectly in a larger system, or vice versa. Correctness is a rather vague and abstract concept and quite distinct from proof. Using a type system, we could prove that, given certain pre-conditions, large state-spaces cannot be visited. Whether it will behave correctly within the reduced state-space, the programmer can only hope. Even formal languages such as Coq rely on correct execution of the assembler, CPU and system environment. I think what Dijkstra was aiming for was not a replacement, but more a grounds-up reeducation of the field. And to a certain extent this is currently happening. Functional languages and techniques are everywhere. I hear people talk about monads, monoids and functors, others embrace reactive programming, which is the coinductive branch of programming. Coq and Idris are finally reaching a larger audience (but still small). However, the larger change is slow and requires a generational paradigm shift. It is exactly the thing you are addressing in your article: do the users of a tool believe they are changeable and changed by the tool (Heidegger)? If they do, they also understand the need for self-protection and focus. Teaching and understanding are indeed the underlying pillars if we want to bring software engineering to a higher level. I think the order in which material is taught greatly influences the mental model of the student. Making multiple iterations, one could start with concepts from category theory and work down with for example Coq, Haskell, LLVM / Assembler, Machine Language/system design, CPU Micro-ops to Digital Electronics. This would lead to view the concept of an LLVM as an implementation artefact of Haskell (which in itself can be expanded to other languages). The mental map becomes relatively machine and system independent. Unfortunately, most programmers nowadays start with an easy language that gives instant reward. It is made difficult for the aspiring programmer in this position to understand the concessions made. |