> In 1954, IBM said FORTRAN would virtually eliminate coding and debugging.
Only because Fortran was viewed as transcribing mathematical notation, which wasn’t considered coding. Coding originally referred to having to work with numeric machine codes. Programming languages like Fortran removed the need for having to deal with how to encode the program for a specific machine, and to deal with human errors in that encoding process (debugging). It didn’t mean abandoning formal specifications that you can reason about with a high degree of precision.
I also want to take the opportunity to point out the concept of notation as a tool of thought, coined a quarter century later by IBM fellow Iverson in his Turing Award lecture: https://www.recurse.com/blog/58-paper-of-the-week-notation-a...
> the concept of notation as a tool of thought, coined a quarter century later by IBM fellow Iverson
Precedence for "the concept of notation as a tool of thought" would have to go to Leibniz, 300 years earlier, in The Method of Mathematics:
> "Whence it is manifest that if we could find characters or signs appropriate for expressing all our thoughts as definitely and as exactly as arithmetic expresses numbers or geometric analysis expresses lines, we could in all subjects in so far as they are amenable to reasoning accomplish what is done in Arithmetic and Geometry.
> "For all inquiries which depend on reasoning would be performed by the transposition of characters and by a kind of calculus, which would immediately facilitate the discovery of beautiful results. For we should not have to break our heads as much as is necessary today, and yet we should be sure of accomplishing everything the given facts allow.
> "Moreover, we should be able to convince the world what we should have found or concluded, since it would be easy to verify the calculation either by doing it over or by trying tests similar to that of casting out nines in arithmetic. And if someone would doubt my results, I should say to him: "Let us calculate, Sir," and thus by taking to pen and ink, we should soon settle the question."
-- https://www.rbjones.com/rbjpub/philos/classics/leibniz/meth_...
Keep in mind that Leibniz invented the notation we still use for calculus today (as well as calculus itself), so this wasn't purely abstract for him.