Tony: your statement that 'all this math... ignores the human element' misses the point. Yes, there is *always* a human element, and human failures are a massive source of problems. No-one said otherwise. What this work does is guarantee that humans are the *only* source of problems.
Why is this a good idea?
Look at the amount of software we trust in everyday life that operates *without* human intervention. Engine control units in cars, microcontrollers in pacemakers, electrical regulation units in trains (a guess on my part, but not unrealistic), microcontrollers in building lifts, communications software in PABXes (before dismissing that, consider what controls emergency phones in lifts and buildings), fire alarm control panels... you get my point.
All of these systems operate with a greater or lesser degree of autonomy, and all are safety-critical; it is therefore crucial that very strong guarantees can be made about every aspect of their operation. It's hard to get stronger than the guarantees provided by proof.