I took a few computer science courses at UT back when Djikstra (not from Djikstra himself, though, from Dr. Nell Dale) was there. Everything in the algorithms class came with formal proofs. Loop invariants were core concepts. The book was not yet published, we spiral-bound photocopy of the draft.
Granted, static type checking is a very minor corner case, but manifold small incremental changes add up. It's untrue that human reasoning has never been replaced with automation, and it's untrue that human reasoning isn't currently in the process of being further replaced.
I agree that total replacement of human reasoning is likely any time soon. However, I'd argue that total replacement of human reasoning implies removal of human desires from the input. (What are programs, if not incredibly formal expressions of what humans desire computers to do? How can we divorce human desires from human reasoning about what is good/desirable?) Science fiction provides numerous examples of how a complete decoupling of computers from human desires can go terribly wrong.
Reasoning is computation. It's one suppressed thought away.
'As economics is known as "The Miserable Science", software engineering should be known as "The Doomed Discipline", doomed because it cannot even approach its goal since its goal is self-contradictory'
Part 1: definitions and motivation.
"Radical novelty" describes something new that is so different from everything that came before it that analogical thinking is misleading and new phrases built by analogy with old phrases are inadequate at best. Thinkers in the middle ages were greatly held back by over-use of analogies. There are many cases where modern society has dealt poorly with radical novelty: relativity, quantum mechanics, atomic weapons and birth control pills. The way our civilization has learned to deal with great complexity is to specialize professions, where each profession abstracts away some amount of information, typically expressed in the range of physical scale of their work. The architect deals with a certain amount of complexity: not having to deal with the large scale of the town planner or the small scale of the metallurgist working for the I-beam manufacturer (my interpretation of "solid state physicist" in this context). Computing is radically novel in the scale of complexity handled by a single profession. The terms "software maintenance" (as if time or use alone, rather than shifting requirements, degraded software), "programmers workbench", etc. are evidence that analogies are misleading and software is radically novel.
Part 2: consequences [this summary is more abbreviated than part 1]
History has shown the natural human reaction to radical novelty is to pretend analogies still hold and to pretend that rapid progress isn't possible. We can't keep treating software like it's just some kind of mechanical device and programmers as assembly line workers stamping out widgets. We can't treat software production as just a new type of manufacturing. Manufacturing-style quality control (testing) is a misleading analogy for software quality control, and formal methods are needed for software. Software engineering isn't about designing new widgets, but about fixing the impedance mismatch between humans as assigners of tasks and computers and executors of tasks. There are a variety of vested interests (Mathematicians, businesses, the military, those teaching software development as widget building, etc.) working against advancement of Computer Science as a field. We need to start by fixing our terminology to stop encouraging misleading analogies. ("Software bug" encourages us to think of programmer errors as things that passively happen, like insects crawling into relays, etc.) The job of a software developer is to show that their designs and implementations are correct, not to correctly execute some set of operations that create a software widget.
"couldn't" is past tense. The GP clearly expects/hopes there's a quick remedy here, and your reasoning about "can't" in the present tense (and implied continuing future tense) doesn't hold.
How about you come up with something else other than "-ism", then we'll talk (maybe).