On the cruelty of really teaching computing science (1988)
A 1988 essay by Edsger Dijkstra on “the cruelty of really teaching computing science” is prompting renewed scrutiny of how programmers should be educated and what “engineering” in software ought to mean. Commenters contrast Dijkstra’s call for mathematically rigorous, formally verified programs with today’s practice-oriented curricula, framework-heavy industry, and the messy reality of changing requirements, arguing over where such rigor is practical and where testing and patterns suffice. The thread also touches on modern formal tools, proof assistants, and LLMs, asking whether advances in automation can finally make Dijkstra’s vision attainable—or whether software is inherently more like gardening than classical engineering.
Role and Feasibility of Formal Methods
- Many agree the essay correctly emphasizes mathematical rigor and formal proofs, especially for safety‑critical domains (aerospace, medical, crypto, kernels).
- Several note current tools (proof assistants, verifiable languages, expressive type systems) make this somewhat practical for medium‑sized codebases, but cost and scaling remain major barriers.
- Others argue that only a small fraction of software justifies this rigor; most work is closer to “residential construction” where rules of thumb and testing suffice.
LLMs and Proof Automation
- Some are optimistic that LLMs will drastically lower the cost of writing specifications and proof scripts, auto‑formalizing math and code and “filling in” proofs with humans guiding decomposition.
- Others report that current LLMs are “really bad” at actual machine‑checked proofs, easily failing combinatorial or detailed reasoning tasks.
- Consensus: LLMs may help with boring glue work and specification writing, but not replace human judgement or solve the specification problem itself.
Computer Science Education
- There is debate over curricula that begin with formal methods and program correctness proofs versus more pragmatic, trial‑and‑error programming.
- One account of a proof‑heavy curriculum reports it was coherent and intellectually satisfying but not obviously practical, and was eventually abandoned.
- Several lament that modern CS often teaches patterns and frameworks rather than how computers work or how to reason rigorously.
Programming Practice, Performance, and “Clean Code”
- Some criticize popular design doctrines (e.g., heavy abstraction, “clean code”) as leading to poor performance and not clearly improving maintainability.
- Others counter that non‑critical code should optimize for maintainability and that modern runtimes can mitigate overhead; performance should be profile‑driven.
- There is broader agreement that many developers function mainly as “framework glue,” with real value coming from architecture and critical thinking.
Programming vs. Mathematics
- Several comments explore whether programming really involves deeper conceptual hierarchies than mathematics, as the essay claims.
- Examples from both sides are given: massive proof projects in math vs. enormous codebases, formal proofs of simple arithmetic in proof assistants, and the difficulty of writing even a correct binary search.
- Some argue programming is essentially discrete mathematics; others stress its physical, operational nature and the centrality of changing, ambiguous requirements.
Testing, Correctness, and Real‑World Constraints
- The essay’s skepticism toward testing is challenged: extensive automated tests, fuzzing, and model checking can prove absence of certain bug classes, at least in theory.
- Practically, most teams settle for “doesn’t usually fail” rather than exhaustive guarantees.
- A recurring theme is that requirements are often inconsistent or unstable, making full formal correctness less valuable than adaptability (“software as gardening”).