On the cruelty of really teaching computing science (1988)
cs.utexas.edu
cs.utexas.edu
The more mathematical proof style that he is advocating for is used sometimes in aerospace (in particular Airworthiness) and medical.
Some might say that his proposed methods only apply to software requiring that level of rigor. It is also really expensive.
I think LLMs could help a lot to lower cost by providing some automation to turn specifications into code. DeepMind has already shown a proof of concept for mathematical theorems using Lean. I have a toy implementation for Isabelle oriented towards SE that works quite well.
There results were impressive, but not sufficient for SWE.
If you note, it completely failed at the combinatorial problems.
SW engineering is details, nuance, and tradeoffs.
The specification problem that lead to an AI winter for expert systems still applies.
If we could create good, exhaustive contracts, programming is easy.
The failure of UML as a code generation tool is a good example.
As LLMs are good at pattern finding, at least within the simplicity bias problem, I do think that they will have utility.
But as an Enterprise Architect, form, complete specifications would completely remove the need for an LLM assistant as I could just write fitness functions and let the developers run with what they wanted.
As we know LLMs are in context learners built of threshold circuits, they simply don't have the ability to consider tradeoffs and details.
Funny enough this post has the smell of an author that wasn't aware of papers that came out in the previous couple years describing the specification problem.
That is, an engineer would design and decompose the problem and the system would help to fill in the gaps in proofs. Sometimes this won't be possible, so the human engineer will need to redefine specifications or insert some intermediate lemmas.
So I'm really interested in the "filling up" part, if you have anything to say about it.
TBH, I haven't written anything impressive, just toy examples that are formally verified.
I imagine making it practical for larger systems would require a lot more work.
Taking this forward would require a lot more work and funding to pay for computation to fine-tune models further.
It's an interesting topic, perhaps good for a startup or a research lab in case one finds a decent monetization stream.
At least with current levels of available staffing. The vast majority of software is being developed more akin to ‘residential construction’ type levels of investment rather than even ‘commercial construction’ or ‘major engineering projects’.
Which makes sense. Rules of thumb work well enough most of the time, and when it’s actually important (say a structure member, ahem, crypto library) then it makes sense to get it looked at more carefully by someone who more deeply understands what is going on.
Though I don’t think we have a solid idea of what those areas are yet, let alone have codified them. So YOLO.
There is no such consensus I can see right now on the software side, and software projects are also a lot more complex than a typical construction project in ways that are hard to quantify.
How would you even define a licensing test that wouldn’t be obsolete in a year or two even?
As an external examiner for CS students I can’t say I’m surprised. They aren’t taught science anymore, they’re taught practices and patterns, and since nobody knows how a computer actually works or how to write performant code it’s easy for various grifters to sell them nonsense.
I mean, how well would Clean Code, SOLID and to some degree Agile really sell if people knew the key people behind these things haven’t worked in software engineering since 20 years before Python was even invented? Probably not so well.
If it's not on the critical path, what difference does it make? Code outside the critical path should be optimizing for something and maintainability is as good as anything.
> Especially because Clean Code doesn’t actually seem easier to read or indeed maintain
If that is true, then there is indeed no point in applying Clean Code. But I disagree with GP that Clean Code leads automatically to bad performing code. That depends on your language and execution environment. A JVM is very good at effectively removing vtable indirection if they are not needed at runtime.
There's also other issues with this paradigm, like creating objects out of the arguments to a function. That not only makes your code less maintainable (what if you need a subset of the variables), but now you'll have to drag all that data to each function you create.
Clean code is, IMO, worthless, data- and domain-driven design practices accomplish the goals of clean code better than it the paradigm itself does, and also improve other considerations like correctness and performance.
An interesting question, but a SoA isn't necessarily better than an AoS: it depends on the access pattern, so the question is whether this optimisation could be added as a part of PGO..
I think my issue with clean code is primarily that it doesn’t actually make code more maintainable. As another poster mentioned, data or domain driven design does the same thing better.
I am no biographer of Djisktra’s, so is he being unrealistic about programmers here, or does he not have exposure to what a mathematician would consider Mathematics (Wikipedia entry claiming him a mathematician or no)?
This is not really true. There were complex multilayered systems before computers. In large systems, Western Electric #5 Crossbar was comparable to a large real-time program. General Railway Signal's NX system had the first "intelligent" user interface. But that level of complexity was very rare.
Both mechanical design and electronic design are harder than program design. The number of people who did really good mechanism design is tiny. There were only two good typesetting machines, over most of a century - Merganthaler's Linotype and Lanston's Monotype. Everybody else's machine was a dud. In the printing telegraph/Teletype business, Howard Krum and Ed Klienschmidt designed the good ones, and the other twenty or so designs over many decades were much inferior. There were been lathes for centuries, but all modern manual lathes strongly resemble Maudsley's design from 1800.
There are far more good programmers than there were good mechanism designers or electronics engineers. Programming is not really that hard by the standards of other complex engineering.
That’s a good example and of course it immediately brings to mind TeX, which is an equally monumental if not greater achievement. Certainly there’s no denying that TeX has considerably higher dimensionality than the pre-computerized hot type setting machines. Especially when you include all the ancillary stuff like Metafont.
Also recall that Dijkstra was a systems programmer in his industry career. He was well aware of the complexity of the computing hardware of the day—which was cutting edge electronic design. The semaphore wasn’t invented as a cute mathematical trick; he needed it to get hardware interrupts to work properly. Something which THE managed and Unix, among others, never quite did (although it did get to mostly good enough if you don’t mind minefields).
> There are far more good programmers than there were good mechanism designers or electronics engineers. Programming is not really that hard by the standards of other complex engineering.
Most programmers are incapable of writing a correct binary search, let alone something the size and complexity of TeX with only a handful of relatively minor errors. Programmers capable of that level of intellectual feat are indeed few and far between. I suspect they’re more rare than competent EEs or MEs.
Most programmers are more comparable to the guys cleaning the typesetters, not the ones designing them.
TeX didn't come out of nowhere. It's a successor to the macro-based document formatting system which began with RUNOFF and went through roff, nroff, tbl, eqn, MM, troff, ditroff, and groff. The last remaining usage of those tools seems to be UNIX-type manual pages. There was so much cruft a restart was required.
And don’t just gloss over TeX’s astounding correctness. It’s a truly remarkable feat of the human intellect to design something so large with so few errors.
[1] https://yurichev.com/mirrors/knuth1989.pdf
[2] https://ctan.math.utah.edu/ctan/tex-archive/info/knuth-pdf/e...
If you exclude the programmers who are incapable of writing FizzBuzz (who I would consider "not programmers", no matter what job title they managed to acquire), then I'm pretty sure your statement is false.
If you mean "could sit down and write one that worked the first time without testing", then yes, you could be write. But could not write one at all? I don't buy it.
FizzBuzz really is trivial. Binary search on the other hand is deceptively tricky[1]. It was well over a decade from its discovery to the first correct published implementation! No doubt if asked to write it, you'd look it up and say that's trivial, all the while double checking Internet sources to avoid the many subtle pitfalls. You might even be familiar with one of the more famous errors[2] off the top of year head. And even then the smart money at even odds would be to bet against your implementation being correct for all inputs.
And if you had to do it just from a specification with no outside resources? Much harder. At least unless you know how to formally construct a loop using a loop invariant and show monotonic progress toward termination each iteration. Which brings us back to the original submission. There are some programs that are pretty much impossible to prove correct by testing, but that can, relatively easily, be shown to be correct by mathematical reasoning. Since this is a comment on a submission by Dijkstra, here[3] is how he does it in didactic style
> If you mean "could sit down and write one that worked the first time without testing", then yes, you could be write. But could not write one at all? I don't buy it.
Yes that's what "correct" means. Code that only works sometimes is not correct.
[1] https://reprog.wordpress.com/2010/04/19/are-you-one-of-the-1...
[2] https://research.google/blog/extra-extra-read-all-about-it-n...
If the implementation language doesn’t automatically prevent that problem (and that is fairly likely), the latter group likely would introduce a bug there.
But that doesn't mean a thing. The barrier to entry is much smaller.
I think he was especially thinking of mathematical logic - he referred to programming as Very Large Scale Application of Logic several times in his writing.
If you ever want to see what it's like for a mathematician to not hand wave anything away, look at excerpts from Bertrand & Russel in principia mathematics (no, not the newton book).
It takes 362 pages (depending on edition) to get to 1+1=2
https://archive.org/details/principia-mathematica_202307/pag...
Of course, just like real mathematicians, in our everyday work we stand on the shoulders of giants, reuse prior foundational work (I've yet to personally write a bootloader, os, or language+compiler, and include 3p libraries), and then hope that any bugs in our proofs are caught during peer review. Like in math, sometimes peer review for our code ends up being a rubber stamp, or our code/proofs aren't that elegant, or they work for the domain we're using them in but there's latent bugs/logic errors which may cause inconsistencies or require a restriction of domain to properly work (ex code only works with ASCII, or your theorm only works for compact sets).
And of course, the similarities aren't a coincidence
https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_corresp...
In practice, one would use a proof assistant, which is like a programming language, such as Agda. Then it is just the definitions and the proof is just a call to the proof checker to compute and check the result.
Inductive eq' {T: Type} (x: T) : T -> Prop :=
| eq_refl': eq' x x.
Inductive nat' :=
| zero
| succ (n: nat').
Definition one := succ zero.
Definition two := succ (succ zero).
Fixpoint plus' (a b: nat') : nat' :=
match a with
| zero => b
| succ x => succ (plus' x b)
end.
Theorem one_plus_one_equals_two : eq' (plus' one one) two.
Proof.
apply eq_refl'.
Qed.
We would also have to be satisfied that the definitions of eq', one, two, and plus' above sufficiently match up with what we mean by those concepts.
> ... is he being unrealistic about programmers here, or does he not have exposure to what a mathematician would consider Mathematics?
As with any sweeping statement, Dijkstra's assertion is not universally applicable to all programmers. However, for some definition of sufficiently skilled programmer, it is correct if one considers the subset of mathematics applicable to provably correct programs. To wit:
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
Take for example a single theorem: Classification of Finite Simple Groups [1]. This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete.
Fermat’s Last Theorem [2] took 358 years to prove and required the development of vast amounts of theory that Fermat himself could scarcely have imagined.
[1] https://en.wikipedia.org/wiki/Classification_of_finite_simpl...
Now compare that to google3 or any other large software. It’s absolutely tiny. A paltry edifice in comparison both in pages and man hours as well as mathematical complexity. Boolean structures get monstrously huge.
On the subject of proofs and the verbosity of traditional mathematical methods, this note[1] is interesting. It provides two fun little examples of shorter than normal proofs.
It amuses me that just as mathematicians persisted in writing out “is equal to” for decades after Recorde gave us =, there will probably continue to be holdouts who write out “if and only if” instead of using ≡ for many years to come.
[1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD107...
https://en.wikipedia.org/wiki/Logical_biconditional has some nice comparisons of notation, including a mention that my old friend George Boole also used '='.
It was first published in 1976. It is _highly_ unlikely Dijkstra didn't know about it.
And yes the average mathematical theory is indeed flat compared to a large monolith like google3.
So true today in the age of identity theft, data breaches, privacy violations, deep fakes, surveillance, copyright violations, tracking cookies, fake news, addictive social media, computer viruses, ransom attacks, ...
But, hey, at least we have ChatGPT now that can write your homework for you.
Do the people agreeing with the article agree with its actual point? Especially whether it was wise before AI (maybe) improved the practicality of such an undertaking?
Those absolutely global formal systems that can explain any kind of behavior would never be practical in general. But specialized formal systems are just great.
In other words, "software is hard": https://www.gamearchitect.net/Articles/SoftwareIsHard.html "The difference is that the overruns on a physical construction project are bounded. You never get to the point where you have to hammer in a nail and discover that the nail will take an estimated six months of research and development, with a high level of uncertainty. But software is fractal in complexity. If you're doing top-down design, you produce a specification that stops at some level of granularity. And you always risk discovering, come implementation time, that the module or class that was the lowest level of your specification hides untold worlds of complexity that will take as much development effort as you'd budgeted for the rest of the project combined. The only way to avoid that is to have your design go all the way down to specifying individual lines of code, in which case you aren't designing at all, you're just programming. Fred Brooks said it twenty years ago in "No Silver Bullet" better than I can today: "The complexity of software is an essential property, not an accidental one. Hence, descriptions of a software entity that abstract away its complexity often abstract away its essence.""
I prefer a conceptual model more like "Software as Gardening". https://github.com/pdfernhout/High-Performance-Organizations... "Andy Hunt: There is a persistent notion in a lot of literature that software development should be like engineering. First, an architect draws up some great plans. Then you get a flood of warm bodies to come in and fill the chairs, bang out all the code, and you're done. A lot of people still feel that way; I saw an interview in the last six months of a big outsourcing house in India where this was how they felt. They paint a picture of constructing software like buildings. The high talent architects do the design. The coders do the constructing. The tenants move in, and everyone lives happily ever after. We don't think that's very realistic. It doesn't work that way with software. We paint a different picture. Instead of that very neat and orderly procession, which doesn't happen even in the real world with buildings, software is much more like gardening. You do plan. You plan that you're going to make a plot this big. You're going to prepare the soil. You bring in a landscape person who says to put the big plants in the back and short ones in the front. You've got a great plan, a whole design. But when you plant the bulbs and the seeds, what happens? The garden doesn't quite come up the way you drew the picture. This plant gets a lot bigger than you thought it would. You've got to prune it. You've got to split it. You've got to move it around the garden. This big plant in the back died. You've got to dig it up and throw it into the compost pile. These colors ended up not looking like they did on the package. They don't look good next to each other. You've got to transplant this one over to the other side of the garden. --- Dave Thomas: Also, with a garden, there's a constant assumption of maintenance. Everybody says, I want a low-maintenance garden, but the reality is a garden is something that you're always interacting with to improve or even just keep the same. Although I know there's building maintenance, you typically don't change the shape of a building. It just sits there. We want people to view software as being far more organic, far more malleable, and something that you have to be prepared to interact with to improve all the time."
And it helps to keep things simple. https://www.infoq.com/presentations/Simple-Made-Easy/ "Rich Hickey emphasizes simplicity’s virtues over easiness’, showing that while many choose easiness they may end up with complexity, and the better way is to choose easiness along the simplicity path."
Most developers I have worked with are cowards exactly as he used that word. Now in all fairness my career is largely limited to large corporate employers that only hire Java developers and, god forbid, JavaScript developers. It’s frameworks, Maven, and NPM for absolutely everything.
The hiring managers always claim to look for innovators, but then you get in and everyone is just the same. Thousands of developers just retaining their employment doing the same shit day after day, fearing any changes coming down the pike.
I can't recall the last time I saw a hiring manager looking for an innovator.
Most hiring managers want people who can just get the job done with as little supervision and involvement as possible.
Most of the time when I see a coworker going off and innovating, it's a questionable exercise designed for fun and entertainment rather than getting the job done.
My last job had someone spend months "innovating" an all new custom CI/CD system. It brought no benefits to the team and was a huge waste of time. They had fun and used it as a major accomplishment their resume and LinkedIn. You could say it was "innovative", but the rest of use really wished they would have helped us out with the work that had to be done instead of "innovating" off in the weeds.
A lot of people (especially newer profiles I've seen on HN) think just being able to glue libraries together is enough to justify being a developer with a 6 fig salary, when in reality the actual value add is the architecture, design, and other critical thinking actions.
Hiring managers do try to hire the archetype developer who is both eloquent and a critical thinker, but it's hard and those who can do both know their value.
Plenty of code monkey types flamed out or remained underemployed.
> the 5 fig salaries I was offered last century, fresh out of school and still wet behind the ears
And there were also fewer developers in the 1990s/2000s than in the 2020s, and the hiring market was not yet fully globalized and async compared to the post-COVID WFH/Remote market.
> I have met some developers in my career that can communicate as effectively as this with equally brutal criticality, but those people are astonishingly rare
The fact that it's rare to find arrogant people who argue with "brutal criticality" that all programmers should use formal methods all the time (like Dijkstra did), is not a bad thing IMO.
I thought that they were looking for "rock stars". Not the same thing...
As brilliantly composed as the piece may be, it exhibits the same resistance to radical novelty that it condemns. Here we are not 40 years later, and small changes to big networks produce small effects. At sufficient scale, the digital reapproximates the analog.
You're talking about bio-mimetic systems that wouldn't arise for a generation, he was talking about "the discrete world of computing". There's no context there to resist.
We built large statistical systems out of the "discrete world" components. Different regimes, if you will.
The fascinating thing is that chemical/biological systems evolved discrete interactions (e.g. nervous systems that can be deranged by, say, a few micrograms of LSD.)
- - - -
Also, Cloudstrike/Clownstrike: small change, large effect?
For the shape Q, instead of clipping opposite corners of the 8x8 square board, one (what would lay under a) white square and one black square, which are non-adjacent, are randomly removed.
Real world programming is usually like this, it is hard to cast the problem in the framework of a formal language, like first order predicate logic, and manipulation of uninterpreted formulae (i.e. the problem now mapped into the domain of first order logic) using the rules of first order logic might not lead to anything useful.
It seems to me that EWD is showcasing some example programming problems that are elegantly handled by his formal proof techniques, while ignoring the vast swathes of programming problems that might not be well handled by these techniques.
(Much more generally, Hall's marriage theorem characterizes which finite bipartite graphs have a perfect matching, and there are polynomial-time algorithms to compute maximum cardinality matchings in arbitrary finite graphs.)
Typically people have insisted that it's too expensive to prove software correct, but as the machines and techniques improve proven-correct software becomes cheaper and cheaper.
The last argument standing is that it's unpopular.
Most software development is wrestling with malleable requirements.
As the old joke goes: writing software from requirements is like walking on water, both are easy when frozen
Automating BS is bad.
> Thus, you could say there is no correct answer.
I object to such fatalism.
Kind of the whole point of computers is to find and eliminate such ambiguities.
I don't mind playing irrational games for entertainment, but they are "no basis for a system of government", eh?
> Most software development is wrestling with malleable requirements.
Sure but that's no excuse for automating irrational systems. There's no written requirement that the math to compute totals and taxes shall be mysterious?
What's the general solution in the random non-adjacent opposite-colour case, out of only the slightest curiosity?
The part where you notice the two paths are even length feels a bit like dark magic the first time you see it. Notice that if you have two different coloured squares which are consecutive on the cycle the paths you get are length 64-2 and 0, then if as you move one of them further and further along the path you have to move in steps of 2 to keep them opposite colours.
You have to verify though that the Hamiltonian cycle exists. An induction proof seems to do the job.
On the other hand, a program's correctness doesn't depend on human beliefs. It can be proven to work perfectly on certain ranges of inputs by actually executing it on those inputs. Human subjectivity can be factored out to an increasing degree by way of automated tests. This level of concrete proof exceeds the level of social proof which mathematics relies on. The electronics upon which programs execute do not have biases as humans do. Evaluating a complex mathematical proof is as prone to errors as humans evaluating a complex computer program with their own minds. The compiler will always beat the human when determining correctness of a program for a well defined range of inputs.
Although automated tests can rarely prove universal truths, they rarely need to, as the logic they test only needs to handle a limited number of inputs and requires a limited number of guarantees. For many programs, the degree of proof that a well written automated test can provide far exceeds the degree of proof that a mathematical proof (based on human consensus) can provide.
This is why programming can accumulate complexity at a rate which is unfathomable in mathematics. With AI, programming may exceed the capabilities of mathematics to such extent that the entire field of mathematics will become a historical relic; showcasing the desperation of feeble human minds to grasp truths that are well outside of their reach.
The 'importance' of the field of knowledge comes down to the scale of the information and growth speed of the field. For all practical purposes, it seems that the programmatic, exhaustive approach will beat out the mathematical approach of trying to solve problems by uncovering universal truths.
Also programming is based on mathematical ideas. I don't think you can do away with mathematics just because of AI.
Math and computer science just happen to be two fields which concern themselves with different aspects of logic. Math being slow-moving and focused on solving universal problems and computer science being fast-moving and focused on solving concrete problems.
Once in a while, advancements like cryptography and LLMs show us that focusing on solving concrete problems can also expand our knowledge and capabilities in a radical (and useful) way.
I resent articles which try to present one as more important than the other. What does that even mean? Appeal to academic authority? Utility value? Difficulty? Degree of abstraction? They're both just languages which solve problems in different ways and which have different target audiences and have different scalability constraints.
I strongly agree with about half of the essay, while I want to agree with the other half in principle, but instead I think it is indeed "...so ridiculous that [he is] obviously out of touch with the real world".
In Peter Seibel's Coders at Work, the interview of Knuth includes
""" Seibel: Yet Dijkstra has a paper I'm sure you're familiar with, where he basically says we shouldn't let computer-science students touch a machine for the first few years of their training.; they should spend all their time manipulating symbols.
Knuth: But that's not the way he learned either. He said a lot of really great things and inspirational things, but he's not always right. Neither am I... """
[Much more of interest, but I don't have the time to type it out now.]
Wrong.
> Instead of teaching 2 + 3 = 5 , the hideous arithmetic operator "plus" is carefully disguised by calling it "and", and the little kids are given lots of familiar examples first, with clearly visible such as apples and pears, which are in, in contrast to equally countable objects such as percentages and electrons, which are out. The same silly tradition [...]
This guy would make a terrible elementary school teacher and getting this wrong leads me to believe he's also wrong about the point he's trying to make afterwards.
> Unfathomed misunderstanding is further revealed by the term "software maintenance", as a result of which many people continue to believe that programs —and even programming languages themselves— are subject to wear and tear.
If your software interacts with a changing external world, then software does rot. Security vulnerabilites, new protocols, etc all require a change. Your webserver can't serve insecure http in 2024. At least not if you want to build a business on it.
This is indeed sensible. However, you don't have to start with this and you don't have to stick with the easy {black, white}. You could rename the values to "banana" and "left" for increased, although needless, difficulty.
My proposal: Have students write a simple correct program first and then show that it still works even if you rename all "user" variables to "comment" variables. Now "comments" have a "favorite pet", but the software still works. Magic! That shows how semantics and syntax are different, plus how "stupid" computers are, even if you "tell" them "what you want."
At some point I realized that he was ascribing all kinds of meaning to variable names and also felt totally lost at how I "knew" what to call various things.
I first tried to explain that the names were just labels but he wasn't getting it. I immediately changed every single variable name to the most profane and insane random junk I could think of then showed the program still worked the same way. Making it obscene was important; simply changing from one set of reasonable names to another would just leave the impression that there were alias in the list of Magic Words. He was enlightened.
From there we were able to get into what things actually were Magic Words (like language keywords)-- or close enough (variable name set by system or library code that we were using, arbitrarily set by their authors but obligatory for us users). Knowing not everything was magic made a big difference.
It's not just AI that carries the risk of overfitting. Sometimes you need some "out of distribution" material to separate convention from the underlying truth.
> quoted text
Wrong.
> additional quoted text.
It's such an off putting way to start an interaction.
However, I also think that anyone that taught math by jumping straight to the advanced maths would almost certainly find that they lose more than they gain as far as student progress.
Note that this is not to say that you should avoid the advanced stuff. Attempts at hiding complexity never seem to pan out to results. Instead, honesty with the students goes a long long way.
I would also be interested in knowing about all of the things that were a bit more normal in the early days that people today have likely never seen. Call semantics that are not stack based, as an easy example.
You can but nobody does. It's enough if it doesn't usually do these things.
It appears to me to be the worst part of high school math (proofs) without much gain.
I'm really, REALLY, REALLY hoping that AI can help with this stuff, because doing it by hand seems insane.
[1] https://www.youtube.com/playlist?list=PL9o9lNrP1luXgu97NZnQH...
> By now, you may well ask why I have paid so much attention to and have spent so much eloquence on such a simple and obvious notion as the radical novelty.
Maybe this is because English isn't my first language, but doesn't this come off as pretty pretentious? Calling your own writing eloquent, in that same writing?
Anyway, then I scrolled down to the bottom to see who the author was. I suppose he has the right to some pretentiousness.
> In what we denote as "primitive societies", the superstition that knowing someone's true name gives you magic power over him is not unusual
Thats funny, because its not about magic powers but a psychological trick that makes someone seem more trusted when they say your name. Its not about superstition but being able to understand things in more than a direct blunt way.
"We are hardly less primitive: why do we persist here in answering the telephone with the most unhelpful "hello" instead of our name?"
Implying that giving away your name to someone who doesn't know it yet is a similar kind of superstition, but its definitely a sane safety measure, as we know today all the crazy examples of what social engineering and elaborate scamming can do.
Had anyone the same impression or am I not used to reading harder texts?
I think that for example environmentalists, who coined the phrase "think locally, act globally" and contemplated an already existing world population on the order of 10^9, might beg to differ. Or, say, astronomers. Or physicists. Yes, people often have poor intuition about large numbers. No, the resulting problem isn't remotely unique to CS.
> The second radical novelty is that the automatic computer is our first large-scale digital device.
Yet small-scale digital devices such as mechanical relays - or, for that matter, light switches and push buttons - were well established by Dijkstra's time. The scale isn't relevant to that concept; experience is, and students in the 1980s had plenty of reasonable mental models for a bit of data as an abstraction (or the hardware storing it, or a boolean value in a program).
> To do so, however, is highly dangerous: the analogy is too shallow because a program is, as a mechanism, totally different from all the familiar analogue devices we grew up with.
As if students would never encounter stepwise functions in math class (or much stranger beasts for that matter)... ?
Metaphor and analogy are simply at the core of how people naturally learn. We are not machines that can be deliberately and directly programmed with an understanding of novel systems. The imperfections of the metaphors we use, are no more a problem than the leaks in the abstractions we create in our programs.
> Unfathomed misunderstanding is further revealed by the term "software maintenance", as a result of which many people continue to believe that programs —and even programming languages themselves— are subject to wear and tear.
I can only imagine what Dijkstra would think of today's "ecosystems".
I wonder how evergreen this essay will be.
- pure maths: algorithms
- physics and chemistry: how to build physically from "scratch" a computer.
Namely, without a strong scientific background, you just are a script kiddy until you decide to go thru years of really tough learning. Why do you think high school kids can code assembly which gets the job done?
What we call "tech", is just "usage implementation", but there you get full frontal with the worst the human kind can deliver in falsehood, toxic excess, etc.
So when you come from the "clean and pure" (well, you have smart and evil people)... computer sciences field, hitting this toxic diarrhea, this "usage implementation", because you need to have the job done, ooooof!
My copium: stay as close to the bare metal as possible using a near-0 SDK and aim for the very long run, but you will have to fight complexity where it does not belong, like the javascripted web, many file file formats (for instance runtime ELF), and for that, better get your lawyer ready and start to enlighten your administration for regulations, because you will have to deal with the (big) tech mob.
Each of the dozens of ECUs in todays cars have a plentifold of complexity compared to any system existing in 1988.
Still a majority of people are managing to operate such a vehicle with as biggest aid, exactly the naive abstractions that he lamented about. The highly simplified mental model that we create of anything we interact with, is the biggest human strength, while he seemed to advocate quite the opposite.
For most students this wasn't easy, particularly compared to the way most of them were comfortable programming on their own by trial-and-error hacking away at a problem. Proving programs correct by construction takes a different skill. At the same time, it wasn't particularly hard either once you got going.
I don't think this way of teaching and learning programming was very useful or practical. With Dijkstra's students leaving the university, or otherwise losing primacy at the computer science faculty, Dijsktra's ideas faded away from the curriculum. Since then—I returned twenty years later to teach at this university—, the curriculum is very like any other computer science / engineering curriculum. And students seemed to have as much trouble with it as before.
What I missed about the curriculum when it was gone, was the consistency it brought into the curriculum. The curriculum felt as one continuous track to some clear idea of what it meant to be a programmer in Dijkstra's style. If you liked that idea, the curriculum was a great guide. If you didn't, it felt as a waste of time.
This is only a viable strategy insofar as the tool which lets them hack away is itself correct. You need computer scientists producing these tools.
- DJ
Edit: "Then reduce the use of the brain and calculate!" This is literally the worst advice I have ever read.
- DJ
"Programs" without computational models and operational semantics are, for sure, discrete mathematics. But almost no one cares about those abstract programs, except for discrete mathematicians.
I'd say it's Edgar's view here which is the mystification. He wishes to pretend that the state of an LCD screen as it plays a video game is can be defined symbolically, and hence transformed in its definition.
This is nonsense.
Programming has never been discrete mathematics. And all those discrete mathematicians ("Computer Scientists") who wish it so are the origin of all this dumb mystery around it. Computers are useful because they are electrical devices, and through operation, transmit power to connected devices, whose physical state has relevance to us. I move a joystick and the electrical state of the LCD screen (etc.) changes, and so on.
Pretending that this can be given a denotational semantics is the charlatanism by which AI zealots also claim the world is some abstraction.
Huh?
If programs, such as video games, are mathematical objects, then the world is one too. But, of course, they are not. They are physical objects distributed in space and in time -- hence why people play them.
ED's discrete mathematics idealism here is the windmill he's tilting against. This is the origin of the very confusions he's annoyed with.
No, programs are not abstractions, and that is why almost every programmer bothers to write one.
On some substantial points, the author is clearly correct: mathematics has proof checkers and proof assistants, and may soon have AI support as well. Computers are a thing. (Yes, I know who the author is. But I'm critiquing the text, not the person.)
I'll give the author what I think is their central argument: programming is a mathematical-intellectual discipline, not some form of glorified HVAC maintenance where you simply have data instead of water flowing through your pipes. I've never yet had to clean rust off a shell pipeline. More formalised methods for programming (even if they are called 'Rust') and other structures such as type systems absolutely need to be taught and used, where appropriate. Full-on formal methods have their place, but that place is a small minority of all code.
I don't fully agree with the criticism of reasoning by analogy. Surely what matters is whether there really is an analogy or not, or as a categorist would say, you have a morphism not just a mapping. Reasoning about cars from horses doesn't work because there is not much analogy here. Reasoning about the property of the as yet undiscovered Element 31 from the properties of the known element 13 (Aluminium), and the fact that elements N = 14, 15 etc. seemed to be similar to elements N + 28, worked out well. At the time, of course, the analogy was phrased in terms of atomic weights rather than element numbers - the fact that these analogies worked out more often than not led to the hypothesis that there was something deeper going on here, which led to the invention of the periodic table (and element numbers). This is all proper Science (TM), not mediaeval scholasticism.
"Programming tools" - look, I like VS code with old-fashioned intellisense, even if you have to turn off the AI crap nowadays. I also like git, for that matter. And syntax highlighting, and visual diff, and compiler errors being red underlined in the source code, and Control+Click on a function name taking me to its definition (usually). I can program in nano when I need to, but not when I have the choice. Maybe for some of the younger generation, they won't be able to imagine programming without an AI copilot. The author here is falling into their own trap, first explaining why mathematics can be revolutionized by tools (such as computers) but then asserting that of course programming cannot. Oops.
I'll give them that perhaps 80% of proposed programming (teaching) tools are rubbish, and maybe that was closer to 100% back in the day, and every few months some new low-code/no-code "solution" appears, but that doesn't mean there aren't good ones out there.
I usually yawn at any mention of the "testing can only reveal the presence of bugs". Yes, and then you can fix all the bugs that were revealed! Well-tested code (that requires some thinking about what to test - see "A QA engineer walks into a bar") has far, far fewer bugs than non-tested code. Some coding interviews expect you to test your code without being told explicitly to do so. It turns out, you can get something like 80% of the benefit of "formal methods" with 20% of the effort, and without having to switch your programming language.