I’ve read a lot from Djikstra, but never this one. After giving it a read, it’s one of his most concise summaries of his overall philosophy. If he’s wrong about anything, it’s how formal methods are not up to speed with the scale of software that we want to build, and that I believe we can never get away from operational reasoning.
I’ve been keeping a bug journal for some time now. It’s very enlightening because instead of making things up, I have raw data about what goes wrong at work, for me. For me, logic errors account for probably 40% of bugs. Another 40% are operational problems, mostly performance related. The rest are typos and unintentional breakages of parts of the program that are unknowingly coupled to something I changed.
All that being said, even when he’s wrong, he’s right. Logical soundness must come first. This cannot be done without math. All programmers are doing math whether they acknowledge it or not, specifically mathematical logic and set theory. Refactors to improve performance must keep the logical function of the program the same.
I believe him wholeheartedly when he says:
> The statement that a given program meets a certain specification amounts to a statement about all computations that could take place under control of that given program. And since this set of computations is defined by the given program, our recent moral says: deal with all computations possible under control of a given program by ignoring them and working with the program. We must learn to work with program texts while (temporarily) ignoring that they admit the interpretation of executable code.
This man understood computation far more deeply than anyone out there today. Today, we have completely baseless claims being spouted like religion. We are in the era of the personality - a person’s personality determines how much they are listened to in our field. That is tragic, and while Djikstra might not have the answer for software of our scale, he has the only correct point of view in my opinion.
I agree a lot with Dijkstra as well, especially when he denounces how childish it is to compare computational processes with physical ones instead of understanding them for what they are (i.e. 'the radical novelty'), but to play the devil's advocate, formal thinking is not how we learn.
I personally find it hard to understand a concept, even in pure math, if I don't understand the motivations that lead to that concept being formulated (not necessarily practical applications, I'm fine with purely theoretical concepts, just why that definition solves a problem, I guess); it's simply too much to ask someone to "get" programming without an intuition of what types of problems it solves.
The fact that more and more people get into programming, even professionally, without proper mathematical fundamentals is another topic entirely.
I cannot imagine a mathematics lecturer telling his students "a monad is like a burrito". Sometimes I think the analogies can actually hurt our understanding of something very abstract or novel, as is the case with the bad burrito analogy.
I completely agree with that but my angle was slightly different. Burrito monads are the prime example of what not to do, but my university course on category theory didn't start with the lecturer throwing out definitions, it started with an explanation in plain English (well, it wasn't English but you get the point :)) of what the theory is trying to accomplish. I'm completely behind the Dijkstrian viewpoint that computing is a radical novelty in itself, but I don't see why trying to explain the purpose of what you are doing is bad.
To make a more low-level example, pretty much every explanation ever of the concept of R-module started with 'we are trying to generalize the concept of a vector space to sets that have a ring structure but not a field structure', not 'here, have a bunch of axioms'.
> I cannot imagine a mathematics lecturer telling his students "a monad is like a burrito".
Well of course that's fatuous-- a math teacher's job in this case is to explain category theory. It would be professional malpractice for them to use an analogy to justify not teaching category in the interest of teaching practical programming techniques.
If one wants to learn what the Monad abstraction is, then one by definition will have to learn some category theory! I don't think there is any need to understand what a monad is in order to use any practical programming language. My point was that the burrito analogy does more harm than good (as predicted by Dijkstra).
> If one wants to learn what the Monad abstraction is, then one by definition will have to learn some category theory!
Actually, I always thought people were referring to Doug Crockford's talk about monads where he makes an offhand analogy to burritos at the beginning. In that talk the analogy has absolutely nothing to do with the 45 minutes of slides he presents, so it always struck me as weird. I had no idea bloggers had actually used a burrito analogy to explain monads-- I now realize he was making an allusion to that.
At any rate, in his talk he explicitly avoids both category theory and type theory in an attempt to explain monads to Javascript programmers for practical programming purposes.
The way I've thought about it is that we cannot understand a problem until we've faced it ourselves.
And too often we try to teach each other by going straight to the answer, and then it just doesn't stick.
I recall this happened to me when reading about 'soft' skills (such as collaboration methodologies), it wasn't until I was working with a team of people at a job and was faced with the problems these methodologies attempt to solve that I was able to read about them without immediately thinking "this sounds like bullshit"
I think this is part of why the "Learn X the hard way" method of teaching can be so effective. It's forces you to solve a problem with foundational tools.
> “Logical soundness must come first. This cannot be done without math.”
I’ve long had this (mistaken?) belief that formal methods and mathermatics do not primarily apply to the areas of computing I’m involved with.
I am involved with business systems that are primarily concerned with the recording of activities. Those activities relate to thing/s, and often involve people and places acting in some role (context). In some ways I am modeling interactions between phenomena, together with the concepts through which they are abstracted. Consider for example a payroll system or a airline reservation system.
How can formal methods and mathematics help in this?
These systems are in one sense ideal for formal methods: they're complex interactions between systems, often coordinating over resources and time, with many easily identified constraints that must be maintained.
On the other hand, they're awful for formal methods to the tune of how expensive and valuable it is to actually get a complete description of what the intended behavior of these systems even is.
The bane of application of formal methods in software is that many practical automated systems are only intended to perform against an incomplete, often somewhat inconsistent, and often rapidly changing goal specification. They could be leveraged very fruitfully against these problems, but to do so would invite a long, expensive requirements gathering process between modelers and business owners. There's some anecdotal evidence that this is a valuable process, but the economics don't work out. Even in circumstances where the benefit is obviously there, formal methods front load cost and thus increase delivery risk in many projects.
I think the right way of bringing these techniques to practical software is through expansion "horseback formal methods": lightweight semi-formal tooling and practice which pays out moderate value for moderate investment. These techniques could be run earlier on in a project and demonstrate the value of formal methods while reducing the eventual cost of implementing the heavy hitting tools later on.
A lot of software engineers practice this already, but don't always have the experience to connect back-of-the-envelope domain modeling to mathematical modeling. Or don't find it sufficiently valuable, which is fair. Hopefully, expansion of popularity in these methods will increase the popularity of making smoother transitions from lightweight modeling to more expensive, formal, comprehensive modeling.
Agreed on lightweight formal methods. TLA+ and Alloy have been really eye opening to use, and it's almost at no cost. They're just tools for expressing logic and analyzing models.
Even those are very heavyweight to my mind. I’m thinking things as simple as applying semantics to flow charts and making state tables. Exhaustive enumeration of small spaces forms a neat on-ramp to more powerful methods, if we choose to treat them that way.
Here "horseback" is a term I'm using to mean "applied in the field, cutting corners as needed to make things valuable now". I'm not sure exactly where I picked it up, but I like the idea.
I generally give these business systems the name of "interactive information systems." That's exactly primarily what I work on as well (and I imagine what most people work on, but not all of course).
Maybe counterintuitively, this kind of system is what brought me to math. I kept hearing things like "oh this is just a CRUD app" and it's a solved problem - yet we were opening 50 bug tickets per week (and that's not an exaggeration, we have a large application, and we measure our bug intake and report on it every sprint).
So the first place where math can help with this is at the source - the data! I know not everyone is using a relational database, but the relational model of data is firmly based on math. Learning more about set theory explicitly has improved my interactions with our relational DB immensely.
In my experience, I was taught data access through ORMs. Honestly, the relational model is so much simpler and more elegant. I read somewhere that Edgar Codd used to express relational queries using only predicate logic notation, and I imagine that that would be so much simpler than SQL, and certainly more simpler than bloated ORM code.
On the query front, we like to treat the database as an implementation detail, but I find that this is not practical. Practically, lots of domain logic has to live in queries. I have had 2 bugs recently where a query itself was not returning the right data. Improving my formal reasoning via sets and predicate logic has improved my querying immensely.
I may be wrong, but it seems your design architecture is similar to “structured design”. Where you model data, and alongside that the transformations to be performed on that data. Traditionally this might have been documented using entity-relationship and dataflow diagrams.
In our case, we model our complex business problem domain using an object model independent of persistence and any particular user/system interaction. Perhaps unusually for these days, we also model the many constraints (business rules) within the object model.
Given that the nature of our domain model is not based on transformations that I guess are more easily quantified (or as Dijksta would say “calculated”), I’m still unsure that formal methods would apply or bring any benefits to us at large, other than perhaps some areas of specific behavior?
they can help you avoid malformed requirements. and/or preempt situations such as "oops your reservation has vanished because a bug; but now thanks to your complaint we've fixed it!"
I don’t think this author understands Dijkstra’s essay the way I understand it. Dijkstra was very specific about advising people to not assign agency to computer programs, nor to rely on operational reasoning. However, the cited examples involve either the explanation of the concepts of programming (rather than reasoning about a program itself), or the very same thing that Dijkstra exhorted us to do... read what the program “says”, i.e. its denotation. Reason about it mathematically and logically, deducing its nature, instead of watching it like a mechanism and abducting various properties.
Exactly. The author misunderstood Dijkstra's essay entirely, or perhaps just wanted to stir up controversy.
Furthermore, it's ridiculous to condescendingly imply that Dijkstra was simply unaware of Piaget whose work was already at the height of popularity well before that time.
Here's the original, which, 32 years later, is still a much better read than this critique of it!
>Furthermore, it's ridiculous to condescendingly imply that Dijkstra was simply unaware of Piaget whose work was already at the height of popularity well before that time.
It's not so condenscending given that his entire essay is basically a bunch of unsubstantiated hot takes, for example:
" It is probably more illuminating to go a little bit further back, to the Middle Ages. One of its characteristics was that "reasoning by analogy" was rampant; another characteristic was almost total intellectual stagnation, and we now see why the two go together. A reason for mentioning this is to point out that, by developing a keen ear for unwarranted analogies, one can detect a lot of medieval thinking today."
This is essentially the unreflected pop-culture reading of the middle ages as the 'dark ages' (I also have no idea how Dijkstra determined that reasoning by analogy was particularly a feature of medieval society), which happens to be wrong, and ironically is in itself a sort of sloppy analogy of the kind he just denounced
> ironically is in itself a sort of sloppy analogy of the kind he just denounced
I read it as that being the point, that analogies are sloppy, reasoning by analogy is sloppy, and look at how this sloppy analogy is intellectually bankrupt.
I fail to see why reasoning by analogy is a problem. After all, the utility of a formal system lies in the way it's elements and rules map to some world context. .. in which case when we "reason" with the formal system we're invoking the analogy to actually conclude something about that world context.
> [T]he utility of a formal system lies in the way it's elements and rules map to some world context.
To some [specific] world context, yes, but not to any world context.
Reasoning from analogy posits that the inverse is true: We can choose an outcome, then use a series of analogies to connect the evidence we have at hand to that outcome. This series of analogies is then codified into “knowledge”.
For a humorous take on this look no further than the witch trial scene in Monty Python and the Holy Grail.
Argument from analogy is a special type of inductive argument, whereby perceived similarities are used as a basis to infer some further similarity that has yet to be observed. Analogical reasoning is one of the most common methods by which human beings attempt to understand the world and make decisions.
The python reference indicates you imply a form of fallacious reasoning which the general "argument by analogy" isn't. The below is a good example I found though -
"There are seven windows given to animals in the domicile of the head: two nostrils, two eyes, two ears, and a mouth...From this and many other similarities in Nature, too tedious to enumerate, we gather that the number of planets must necessarily be seven."
– Francesco Sizzi, 17th-century Italian astronomer
The problem with arguing by analogy is that there are two possible cases:
1. Your analogy maps precisely, in which case it's no simpler than arguing about the original thing.
2. Your analogy is imperfect, in which case your conclusions are suspect.
Case #2 is most common, and the argument usually continues by proposing a different analogy. Now you're arguing about the merits of your analogies, rather than about the topic itself.
Analogy can be a good pedagogical tool, highlighting some aspects of the problem, and giving you an intuitive way to connect to them. But eventually the analogy always breaks, and now you've got to un-learn the analogy before re-learning the reality.
Formal systems aren't arguments, they're assumptions. As long as the assumptions hold, the formal systems are useful. If there's anything to argue about, that's a limitation of their utility.
This feels like a criticism that takes the straw man version of dijkstra's essay and burns it. Too easily, all told.
I have issues with how he is often portrayed, but I have rarely seen Dijkstra portrayed as ignorant. The more common view is of arrogant. Even from friends that completely valued his cutting remarks.
Such that this feels more like a piece designed to get visibility from attacking a great in the industry. :(
> In 1988 when Dijkstra wrote this piece, cognitive science journals were only about a decade old, and learning sciences wasn’t established until the 1990s.
Cognitive science is a re-branding of earlier work in psychology, and constructivism has been around since the late 50's (see Jerome Bruner's work).
It's potentially a sad commentary on academia that fields appear to ignore other fields more than N hops away, where N>=2.
I really like that there is active research being done in this area.
It's interesting to see a constructivist lens applied to teaching concepts in computer science, and I would agree with the author that Dijkstra's insistence on a "blank mind" is the wrong approach. It seems like it would limit learning to those who "just get it", especially for introductory concepts that are typically taught to students who don't have the maturity to dive into abstract reasoning straight away.
It appears to me that the problem with reasoning by analogy is that we often focus on how x is analogous to y, but skip over the part where we think about how x is not like y. Without intentionally making that step, we bring a lot of unwanted assumptions into our understanding of x because we haven't focused on the ways it is different.
> we often focus on how x is analogous to y, but skip over the part where we think about how x is not like y.
Yes! Regardless of whether Djikstra is 100% right or wrong about "radical novelty", software engineering is relatively more novel than more familiar activities (is that phrasing tautological?). Analogies are comforting, because they make a strange thing look less strange. But we have to take both sides of the cut: we can compress our knowledge based on these similarities, while carving away those same similarities to highlight the differences in their own right.
A well-posed set of analogies can surgically lay out the internal structure of a concept. (But we still have to grapple with the pieces!)
Here is an interesting study showing that our solution to a problem greatly depends on the metaphors used to describe the problem. This isn't necessarily good or bad, but it does mean we may think we are coming up with solutions to the problem but be unaware that we are greatly constrained by the words used to describe the problem.
Ooooh, yes, I remember talking about this article with a coworker some months ago.
> we are greatly constrained by the [metaphors] used to describe the problem.
Linguistic relativity might be controversial, but this, I feel, is a "correct" kernel of that idea. (Forgive the slight recombining of your sentiment!)
If you use for example category theory words like “monad” you know what it can do but even better, what you can’t do which is very important when building algorithms. Sure you can say tacos instead but something gets lost.
Unfortunately, the part left out of the analogy - that which is different - tends to be the more complex part.
So although we may be able to establish a baseline along analogous terms - and may be able to use that understanding adequately well in explaining the deeper concepts (or underlying truth) we do need to get to a point of understanding where whatever analogies we used to scaffold out explanation can be discarded.
Which leaves me wondering the depths to which we must be expected to delve to explain a deeply technical subject matter in a university context - and what the scaffold actually achieves.
Folks are fond of asserting the computing is lost without math. Yet probably the vast majority of it is written without formalisms of any kind. And the world is still here.
So, if all it takes is for programming languages to be 'formalism', then pedantically speaking, we're all doing it right. Thanks! My programs are all correct now?
"Formalism" is a fancy word for saying that a system has to have an agreed upon shape - hence form. Programming languages have structure - you can't just type random text, there is a specific syntax, with specific semantic rules based on what you type.
So all I'm saying is that you are working in a formal system, and you are creating formal logic. Every day.
That has nothing to do with correctness. In logic, there is a difference between validity and soundness. A valid argument is one that is in a proper form. You can make valid arguments that are completely untrue.
A sound argument is one that is valid and also happens to be true. It's trivial to create a valid program - it either compiles or is executable by the interpreter. But that has nothing to do with soundness.
It's quite ironic. The unwillingness to understand something, such as math and logic in this case, leads to criticizing it. You can't evaluate what you don't understand.
I did, using the word 'formalism' to perhaps inaccurately describe all the formalisms just discussed (proofs etc). Then it went off into the weeds on that word, which was not helpful.
I'd agree with Dijkstra, provided that he wrote about individual human beings, rather than computers. It is humans that are characterized by radical novelty, not computers, which can be understood by metaphors. It is easy to predict computers (that is why they are useful), and impossible to predict humans.
Category theory was founded on topics like algebraic topology, so there's actually a rich framework of analogies to draw on between the two topics. The problem is, most of us aren't algebraic topologists.
I want to find a better set of analogies between category theory and software engineering, that aren't so coupled to yet other fields of mathematics. I feel like they exist, but in a lot of ways, I'm still in the pre-rigor phase on category theory :(
The newfangled ways of teaching how to code managed to produce a generation of really poor-quality software "engineers" producing atrocious slow and buggy bloatware.
You cannot be a good engineer if you reason with analogies and metaphors instead of understanding how things actually work, at multiple levels, and knowing what and when can be abstracted and which lower-level details are important and should not be ignored.
So... if you want to become a decent software engineer, start with learning digital electronics and assembly. This way you won't need "metaphors" for arrays and such - because you will know that a static array is just multiplication by constant followed by addition to a constant and dereferencing of the resulting address.
Although I agree with the core of your argument, I think this position is a little reductionist. Yes, you really do need to understand what's going on under the hood (though, choose your hood). But you're also almost-but-not-explicitly saying that analogies and metaphors are not valuable tools for engineering. I really strongly disagree with that.
As one example, I find analogies downright necessary when working with a complex domain -- you have to find ways to speak domainese in the software world, or speak programese in the domain world, and analogies are precisely the tool for that job. It's easy to think that domain concepts should have a 1-1 representation in the software world, but in my experience, that's neither true nor productive. You do need to understand (and document for others!) the mappings between those concepts, but they shouldn't be so rigid.
On a related note, I'm reminded of Terence Tao's thoughts on rigor in mathematics [0]. He divides expertice into pre-rigor, rigor, and post-rigor phases. It's necessary to understand the rigorous elements, but those (a) build on intuititons built up over time in the pre-rigor phase and (b) support expert, formalizable intuitions in the post-rigor phase.
> So... if you want to become a decent software engineer, start with learning digital electronics and assembly.
I disagree here too, though less strongly. I think it's important to have approximate intuitions that can be refined, rather than trying to manufacture a precise understanding out of nothing. Those intuitions can be built up by trying, failing, and accomplishing projects that you're motivated by. Even if Djikstra is right about "radical novelty", you obtain a certain amount of mechanical sympathy just by fighting with the computer and learning its needs.
The "Purpose-First Programming" research [1] that this article's submitter also submitted today seems relevant.
I believe you misunderstand how the process of learning occurs. If you really want to deeply understand something, it's a whole process of connecting up existing facts and schemas in your brain. That happens more smoothly over time by processes like seeing metaphors. A good teaching metaphor always involves a description of how the metaphor fails. Learning from metaphors is not a weakness, nor is it the only plank to build a house of knowledge on. Eventually, you will need to understand the mechanics too, but there's nothing wrong with starting with metaphor, or examples, or visualizations, or interactive simulations, or any other teaching scaffold.
Also, don't gatekeep the field, unless you have a citation that proves that modern teaching techniques have really led to a decrease in quality of software engineers. I really doubt you have any concrete measure you can point to that won't be anecdotal, but if you have one I am interested in hearing why you think you can strongly believe that folks have gotten wore over time because we got better at teaching.
> Also, don't gatekeep the field, unless you have a citation that proves that modern teaching techniques have really led to a decrease in quality of software engineers.
I don't think modern teaching techniques have. I think the profession has done admirably (but not good enough) at cultivating the basics in more people than managed it ever before.
But when you multiply the size of the profession by so much, even if teaching improves greatly, odds are you're including a lot more volatility in the amount of ability/intrinsic interest/talent.
There's people who are making it today who'd never have been good enough 20-40 years ago. We need a bunch more programmers and software engineers now, so we tolerate it. And thankfully, improvements in tooling, debugging, and instrumentation, along with a bunch more available performance and storage, limit the harms.
Thank you, I guess. I've been a practicing software engineer for over 40 years now, and watching the decline of my profession over the decades is quite painful.
I think Dijkstra was ahead of time. Whatever you do with computers, you shall not use words like "kill", "master", "slave", "blacklist", "whitelist"...
I’ve been keeping a bug journal for some time now. It’s very enlightening because instead of making things up, I have raw data about what goes wrong at work, for me. For me, logic errors account for probably 40% of bugs. Another 40% are operational problems, mostly performance related. The rest are typos and unintentional breakages of parts of the program that are unknowingly coupled to something I changed.
All that being said, even when he’s wrong, he’s right. Logical soundness must come first. This cannot be done without math. All programmers are doing math whether they acknowledge it or not, specifically mathematical logic and set theory. Refactors to improve performance must keep the logical function of the program the same.
I believe him wholeheartedly when he says:
> The statement that a given program meets a certain specification amounts to a statement about all computations that could take place under control of that given program. And since this set of computations is defined by the given program, our recent moral says: deal with all computations possible under control of a given program by ignoring them and working with the program. We must learn to work with program texts while (temporarily) ignoring that they admit the interpretation of executable code.
This man understood computation far more deeply than anyone out there today. Today, we have completely baseless claims being spouted like religion. We are in the era of the personality - a person’s personality determines how much they are listened to in our field. That is tragic, and while Djikstra might not have the answer for software of our scale, he has the only correct point of view in my opinion.