On the cruelty of really teaching computing science (1988)

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”).