Techniques for Ensuring Software Correctness: What Worked in Past and Present
(Quick revision of 2016 comment on Lobste.rs)
I find it helps to look to prior successes and tradeoffs to try to understand how to best do engineering. People and teams I've identified as independent inventors of software engineering were Bob Barton of Burroughs B5000, Dijkstra w/ THE OS, and Margaret Hamilton in Apollo & 001 Tool Suite. Each had pieces of the problem with some culminating with later work into the TCSEC and Orange Book’s B3/A1 classes of high-assurance security. At IBM, Fagan invented formal, software inspections for lower defects. Harlan Mills invented a method, Cleanroom Software Engineering, that consistently resulted in low defects even on first use. Became my baseline.
In parallel, the safety-critical embedded community continued using all kinds of their own methods or variations on common ones. They often published "lessons learned" reports with useful information. CompSci researchers continued working on