"Often in the evening or at weekends I would bring my young daughter, Lauren, into work with me. One day, she was with me when I was doing a simulation of a mission to the moon. She liked to imitate me – playing astronaut. She started hitting keys and all of a sudden, the simulation started. Then she pressed other keys and the simulation crashed. She had selected a program which was supposed to be run prior to launch – when she was already 'on the way' to the moon. The computer had so little space, it had wiped the navigation data taking her to the moon. I thought: my God – this could inadvertently happen in a real mission. I suggested a program change to prevent a prelaunch program being selected during flight. But the higher-ups at MIT and Nasa said the astronauts were too well trained to make such a mistake. Midcourse on the very next mission – Apollo 8 – one of the astronauts on board accidentally did exactly what Lauren had done. The Lauren bug! It created much havoc and required the mission to be reconfigured. After that, they let me put the program change in, all right."
https://www.theguardian.com/technology/2019/jul/13/margaret-...
In case her work interests you, I did get their book on Higher Order Software where she applied everything they learned. The method was like executable specifications with code generators. The specs were reminiscient of Prolog and CSP mixed together. Later, it became USL in the 001 Toolkit. It and her other papers are on htius.com.
I didn’t think HOS/USL was practical. Her team’s early work was really impressive, though. I also still respect everyone that tried to achieve the hard goal of formally-specified, bug-proof software. Each attempt teaches us lessons.
System Design from Provably Correct Constructs: The Beginnings of True Software Engineering by James Martin https://www.amazon.com/gp/product/013881483X/ref=ppx_yo_dt_b...
https://archive.org/details/systemdesignfrom00mart/page/n3/m...
Now, if you want a practical method, the best were Design by Contract, Cleanroom Software Engineering, and Praxis' Correct by Construction. Cleanroom and CbyC hit very, low, defect rates. DbyC was highly pragmatic in balancing developer productivity, ease of adoption, and correctness. I think they'd all be even better combined with functional programming, static, test generators, etc. that we now have. In any case, here's links to descriptions of and books on some of those methods.
Design by Contract article https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...
Overview of Cleanroom Method https://ifs.host.cs.st-andrews.ac.uk/Books/SE9/Web/Cleanroom...
Book teaching Cleanroom https://www.amazon.com/gp/product/0201385953/ref=ppx_yo_dt_b...
Overview of Praxis Correct by Construction https://elsmar.com/pdf_files/A%20Manifesto%20for%20High-Inte...
Book teaching SPARK Ada with some CbyC https://www.amazon.com/gp/product/1107656842/ref=ppx_yo_dt_b...
Abstract, State Machines and the B Method had many successful, industrial uses. There's many papers on them.