[pron]

Well, software today is much bigger and of higher quality that was thought possible in the seventies. That's not to say that it can scale indefinitely, but my point was that unsound methodologies (i.e. not formal proofs) work much better than expected, and the software correctness world has moved from the seventies' "soundness is the only way" to "software correctness is a complex game of costs and benefits, a combination of sound and unsound techniques is needed, and we don't know of an approach that is universally better than others; there are too many variables".