Here's a nice article on the Nautilus website about Margaret Hamilton: Why Did Obama Just Honor Bug-free Software?
You might call Hamilton the founding mother of software engineering. In fact, she coined the very term. She concluded that the way forward was rigorously specified design, an approach that still underpins many modern software engineering techniques—“design by contract” and “statically typed” programming languages, for example. But not all engineers are on board with her vision. Hamilton’s approach represents just one side of a long-standing tug-of-war over the “right way” to develop software.
Formal methods are very powerful, but also very challenging to use in practice. However, I do believe that they are making progress. For example, in an area that I (somewhat) follow, that of "distributed consensus," there has been quite a lot of progress recently, including
- Lamport's pioneering work on proving Paxos correct
- The TLA work on Raft
- TLA in use for a Distributed Systems class at SUNY Buffalo
- and the TLA team at Amazon
I think you have to be a big, well-funded organization to be able to employ techniques like this, but I'm excited to see their use growing, and hopefully they will become more accessible to practicing software engineers who have less resources available to them.
In the meantime, I've still got Valgrind, and the Address Sanitizer, and my compiler, and my TDD process, so I'll try to emulate Hamilton as best I can...