What he's arguing for is correctness by construction. This is an old idea.[1][2] It was used for the Apollo program, but never seemed to get much traction. The idea is to have small, reliable software components with well-defined interfaces, which are then plugged together. This maps well to certain types of control problems, especially those which can be expressed as classical analog control diagrams with signals flowing around.
[1] https://www.computer.org/csdl/journal/ts/1976/01/01702333/13...
[2] https://en.wikipedia.org/wiki/Margaret_Hamilton_(software_en...