11 ms·

On the cruelty of really teaching computing science (1988)

• firesteelrain 2y ago
  This is obviously a snapshot in time (title includes 1988). I can’t attest to the State of Computer Science Education in the late 1980s. He laments the term software engineering because software engineering does not fit the traditional, more mechanical engineering terms. 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.
  • nextos 2y ago
    We are slowly getting there, SE is just a bit over 50 years old. For example, Dafny (by MSR) is relatively easy to use and scales nicely to build systems of 20-30 KLOC with some formal guarantees. It's a nice imperative language where specifications are encoded as contracts, so quite familiar to developers. Costs are still relatively high obviously, and it won't scale to bigger systems. 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.
    • abelcha 2y ago
      Thats what the ai would say
    • deleted 2y ago
      [deleted]
    • kragen 2y ago
      that's exciting news! what does your toy implementation do?
      • nextos 2y ago
        It translates natural language into Isabelle/HOL specifications, and then tries to fill these up to prove things. One can then use Isabelle code generation facilities to extract Scala, OCaml, etc. I think the trick is to have a programmer to guide the whole process, especially decomposition into different modules and abstractions.
        • kragen 2y ago
          what have you been able to get it to write so far?
          • kragen 2y ago
            (i hope this comment didn't sound skeptical or dismissive)
            • nextos 2y ago
              No worries! The comment was fine, I was simply gone so I couldn't reply. 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.
              • kragen 2y ago
                i'm curious to know what you mean by toy examples! are we talking about an assignment statement, an arithmetic expression, finding the maximum of a list, insertion sort, mergesort, a parser for a context-free language, a cooperative multithreading system?
                • nextos 2y ago
                  Some simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.
    • amw-zero 2y ago
      LLMs are really, really bad at proofs so far in my experience. Especially proofs in proof assistant since those are machine checked and unable to be faked.
    • nyrikki 2y ago
      If you look at the proofs that Google solved, the fast one was similar to problems in Knuth, thus common in the corpus and the other two were reducible to exhaustive search, especially with lean4 feedback. Which is why they took more time than a human was given. 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.
      • nextos 2y ago
        I agree, I am also not interested in a system that replaces humans. I am interested in a system that automates the boring parts and makes SWE simpler and closer to classical engineering disciplines while keeping humans in the loop. 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.
  • devjab 2y ago
    It depends on which parts of software engineering you work in. If you work anywhere where performance matters people tend to know how computers work. If you work in 90% of software engineering you’re likely actively writing code which is terrible from an engineering perspective. Look at how popular things like SOLID and Clean Code in general are. When they are a direct path to horrible performance as you enter the area of L1 cache misses and vtavles on even an extremely simple function. It’s so weird to switch between working close to the hardware and working high above. Especially because Clean Code doesn’t actually seem easier to read or indeed maintain. 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.
    • jimbob45 2y ago
      When they are a direct path to horrible performance as you enter the area of L1 cache misses and vtavles on even an extremely simple function. It’s so weird to switch between working close to the hardware and working high above. Especially because Clean Code doesn’t actually seem easier to read or indeed maintain. 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.
      • funcDropShadow 2y ago
        GP said > 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.
        • 2y ago
  • lazide 2y ago
    Very few domains where software is used now make sense for that level of rigor, in practice. 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.
    • jaybrendansmith 2y ago
      Great post. Yes when your GC or carpenter needs to remove a wall, they bring in a real structural engineer. These roles exist for software engineering also. Only thing we are missing is a real licensing and governance body.
      • lazide 2y ago
        Well, and some sort of stable target to aim at regarding ‘important’. There is pretty solid consensus in construction that things like foundation design, structural walls/supports, projects over a given size, etc. need engineering sign off. 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?
• austin-cheney 2y ago
  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. Maybe 2% of the developer population, if I am being gracious, can be described this way. 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.
  • alephnerd 2y ago
    Frameworks aren't necessarily a bad thing if you can critical think - why reinvent the wheel from scratch everytime when you're trying to make a newer version of a car? But if you're only a framework monkey who cannot communicate design decisions, architecture, and/or design you're definetly screwed in the job market. 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.
    • bulatb 2y ago
      I've always heard that tech employers value all the things you'd expect them to value, but I've only ever seen them value LeetCode.
    • 082349872349872 2y ago
      Then again, just being able to glue libraries together ought to be enough to justify a 6 fig salary, because inflation adjusted that's potentially less than the 5 fig salaries I was offered last century, fresh out of school and still wet behind the ears.
• sneed_chucker 2y ago
  For those who don't know, the author is Edsger W. Dijkstra
  • skemper911 2y ago
    Took 2 paragraphs for me to guess the author ;)
    • copperx 2y ago
      The handwriting was a split second giveaway.
    • 082349872349872 2y ago
      ~1300 EWDs and this one is ~70 paras, so say 100K paras worth of EWDs (+ a similar amount for his published work?) suggesting that 2 paras are still better measured in microdijkstras than in nanodijkstras...
    • d13 2y ago
      2 sentences for me. The enigmatic humorous dirge was a dead giveaway.
    • awanderingmind 2y ago
      Me too! I think it's the pontification presented in a self-aware, humorous way. 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".
      • deleted 2y ago
        [deleted]
  • yen223 2y ago
    He of all people should have been able to find a shorter way to get to the point!
• Gregaros 2y ago
  > The programmer is in the unique position that his is the only discipline and profession in which such a gigantic ratio, which totally baffles our imagination, has to be bridged by a single technology. He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. Compared to that number of semantic levels, the average mathematical theory is almost flat. By evoking the need for deep conceptual hierarchies, the automatic computer confronts us with a radically new intellectual challenge that has no precedent in our history. 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)?
  • wetpaws 2y ago
    [dead]
  • AdieuToLogic 2y ago
    >> He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. Compared to that number of semantic levels, the average mathematical theory is almost flat. > ... 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-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
    • chongli 2y ago
      You’ve given a hint of the complexity on the programmer’s side of things but for Dijkstra’s claim to hold we also need to take a look at the mathematician’s. I think most people who are not mathematicians have no idea what they’re working on. 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_simple_groups https://en.wikipedia.org/wiki/Classification_of_finite_simpl... [2] https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem
• djaouen 2y ago
  Sounds like projection to me. - DJ Edit: "Then reduce the use of the brain and calculate!" This is literally the worst advice I have ever read. - DJ
  • rk06 2y ago
    have you never used a calculator?
• xianshou 2y ago
  From the article: 'In the discrete world of computing, there is no meaningful metric in which "small" changes and "small" effects go hand in hand, and there never will be.' 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.
  • TeMPOraL 2y ago
    Complete with feedback loops and chaos dynamics. Small changes to almost all code would yield small effects. A small change to libcurl or SQLite, creating an application-crashing bug and somehow slipping through tests, would likely halt the world in its tracks.
  • carapace 2y ago
    > it exhibits the same resistance to radical novelty that it condemns 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?
• jongjong 2y ago
  Mathematics is inferior to programming, in a way, because the entire hierarchy of mathematics relies on human beliefs at every stage, all the way down to its axioms. The beliefs of many highly intelligent humans, but beliefs of biased individuals nonetheless. Humans simply can't match the accuracy of a compiler when it comes to finding flaws. 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.
  • fsmv 2y ago
    To be fair we do have computer verified proofs now although it doesn't encompass everything. Also programming is based on mathematical ideas. I don't think you can do away with mathematics just because of AI.
    • jongjong 2y ago
      Agreed, though mathematics and programming as we understand them are both ways for humans to express logic. As much as mathematicians want to believe it, math is not the same as logic. The former serves to express logic to other humans while the latter serves to express logic to both other humans and computers. It's not like in the business world; mathematics doesn't get to have a monopoly over logic just because it came first. 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.
• an-allen 2y ago
  I mean, I’m actually somewhat curious how starting tertiary computer science curriculum with formal methods would impact the students. I mean I felt my intro undergrad 101 course was essentially functional programming and lambda calculus (with Scheme)- and I felt that helped establish a fundamentally different way of thinking about computer science than a more basic procedural type introduction would have. When they moved the intro course to be OOP instead I felt it was a travesty.
  • ht_th 2y ago
    I did follow a curriculum set by Dijkstra's students. In the first trimester, we learned to program in Pascal, so we knew what programming was. The next two programming courses, in the second and fourth trimester, "programming" meant proving programs correct. Using pen and paper. Often in one-on-one sessions with our teachers where we'd to demonstrate our proofs. Or the teacher would state a problem and then continue to derive a correct progam by construction, writing slowly on the blackboard. These programming courses were supplemented with logic, discrete mathematics, and other formal methods. And we had continuous mathematics courses as well, practical labs, electronics, databases, and whatever you'd expect in a computer science and engineering curriculum. 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.
    • mrkeen 2y ago
• taeric 2y ago
  I'm always torn on this. As someone that thinks they are decent at programming, it can be tempting to think that all of the sloppy ways of programming that I learned on the way were bad habits that need to be shed. 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.
• initramfs 2y ago
  fantastic.
• zahlman 2y ago
  > The programmer is in the unique position that his is the only discipline and profession in which such a gigantic ratio, which totally baffles our imagination, has to be bridged by a single technology. 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".
• shric 2y ago
  Somehow I guessed it was Dijkstra just from the title.
• mapcars 2y ago
  I just went to read a random part of the text > 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.
  • xdennis 2y ago
    In this context, true name does refer to magic powers: https://en.wikipedia.org/wiki/True_name https://en.wikipedia.org/wiki/True_name
    • mapcars 2y ago
      The next line kind of makes connection between the two: "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.
• knallfrosch 2y ago
  > the Middle Ages. > total intellectual stagnation 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.
  • knallfrosch 2y ago
    > To further sever the links to intuition, we rename the values {true, false} of the boolean domain as {black, white}. 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."
    • nullc 2y ago
      I was teaching an adult friend some programming-- this was someone who could program "a little"-- mostly smashing stuff copy and pasted from the internet with some brute force until it kinda worked, so I started our exercise at perhaps somewhat of a too advanced level. 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.
• BlueTemplar 2y ago
  What is "chrysocosmic" ??
  • gollum999 2y ago
    I assume it's related to Chrysopoeia: https://en.wikipedia.org/wiki/Chrysopoeia https://en.wikipedia.org/wiki/Chrysopoeia
• sylware 2y ago
  Computer sciences: - 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.
• red_admiral 2y ago
  There are some good ideas here, and this is a historical document for CS like the Gettysburg Address is for the USA, but your average freshman English instructor could offer a lot of suggestions for improvement if this were a class assignment. It could be said in about half the length (something Lincoln was good at!), and you don't need to invoke Galileo every time you're critcizing "the way things are done around here". 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.
• StefanBatory 2y ago
  Was that a talk at first? (EDIT: Because I think it would be very hard to follow it "live") I had trouble going through the points he was making and I had the luxury of being able to read it on my own pace, going back to earlier paragraphs, and so on. Had anyone the same impression or am I not used to reading harder texts?
• Asooka 2y ago
  Dijkstra ironically makes the same error wrt software testing that he is warning against - he didn't envision software becoming so complex as to be impossible to reason about. So today we write small programs to exhaustively test the big program. Automatic tests, fuzzers, tests that click on every possible pixel in every combination, etc. - ultimately the program has a finite number of states owing to its digital nature, so you can prove the absence of certain classes of bugs with enough tests. You can prove it doesn't crash, it doesn't leak memory, it doesn't break authorization invariants, etc.
  • staunton 2y ago
    > You can prove it doesn't crash, it doesn't leak memory, it doesn't break authorization invariants, etc. You can but nobody does. It's enough if it doesn't usually do these things.
• mikewarot 2y ago
  So I read this, and got inspired to learn a bit more about formal methods. I fell asleep listening to this[1] (not because it's boring... just because it was bed time) 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=PL9o9lNrP1luXgu97NZnQH4cxUkEGB5TJ_ https://www.youtube.com/playlist?list=PL9o9lNrP1luXgu97NZnQH...
• ashtami8 2y ago
  In the (is this shape fillable by 1x2 dominoes?) example given by EWD to demonstrate the power of formal reasoning methods, a slight change to the problem statement: 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. makes the elegant proof argument fail. 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.
  • ogogmad 2y ago
    Note that in the adjacent case, a nice recursive algorithm can solve the problem. What's the general solution in the random non-adjacent opposite-colour case, out of only the slightest curiosity?
    • eigenket 2y ago
      Write down a Hamiltonian cycle for the (undirected) graph where the nodes are given by the squares of the chessboard and are connected by edges if they are (orthogonally) adjacent. Notice that because the squares are different colors, deleting them from the Hamiltonian cycle partitions it into two even length paths. Cover each even length path with dominoes. 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.
      • ogogmad 2y ago
        Holy shit that's slick. Wow. You have to verify though that the Hamiltonian cycle exists. An induction proof seems to do the job.
• agentultra 2y ago
  It seems like the author’s conception of medieval thinking is pervasive to this day with LLMs. Systems complex and “radically novel,” enough that most experienced programmers have a hard time discussing them without resorting to analogy and anthropomorphism. I wonder how evergreen this essay will be.
• bsoles 2y ago
  > the business community, which, having been sold to the idea that computers would make life easier, is mentally unprepared to accept that they only solve the easier problems at the price of creating much harder ones. 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.
  • ogogmad 2y ago
    Dijkstra was advocating for using formal methods... 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?
    • pdfernhout 2y ago
      How much value is there in formal proof that a program optimally meets precisely-described requirements if the requirements themselves are sub-optimal for the problem area of concern? In other words, "software is hard": https://www.gamearchitect.net/Articles/SoftwareIsHard.html 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-Reading-List?tab=readme-ov-file#the-pragmatic-programmer-from-journeyman-to-master 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/ 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."
• mjburgess 2y ago
  All useful programs are run on machines with devices whose operation makes that program useful. "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.
  • ogogmad 2y ago
    > Pretending that this can be given a denotational semantics is the charlatanism by which AI zealots also claim the world is some abstraction. Huh?
    • mjburgess 2y ago
      denotational semantics = the meaning of a program is a mathematical object 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.
• robwwilliams 2y ago
  What an amazing educator at all levels. This is worth reading repeatedly until embedded in neurons and practice.
• cafard 2y ago
  CACM gave most of an issue to this, the bulk of the responses strongly disagreeing. The dissenters were not, as I recall, people generally in favor of sloppy coding. 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.]
• whereismyacc 2y ago
  A few paragraphs in the author seemed very pretentious in their writing style. > 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.
  • thisiszilff 2y ago
    Hard to say, as a native speaker eloquence here doesn’t seem to refer to the authors own eloquence but rather the amount of words and roundabout explanations they’ve dedicated to the topic. Ie, in contrast to a simple explanation for the obvious things. If anything it reads a touch self deprecating.
    • whereismyacc 2y ago
      Ah, that sounds fair.
      • abdulhaq 2y ago
        loquacity was the right word
• nuancebydefault 2y ago
  I'm sure that when the author today reads what he wrote, he will ask himself "what the heck was i thinking?" 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.