There exists a body of theory about how to do software engineering as described here, but there doesn't exist a sizable community of software engineers willing

There exists a body of theory about how to do software engineering as described here, but there doesn't exist a sizable community of software engineers willing to do this kind of work on a reasonably large scale. Judging by HN (which itself probably represents the upper-end of 'engaged' software developers), most people fidget uncomfortably when forced to explicitly declare derived types, and gnash their teeth when faced with Haskell monads; who among you would make a career out of writing Coq proofs about system correctness? Optimistically, the community might come around to realizing that this sort of development is at least desirable, and we might wind up with the basic components of popular OSes, or of firmware for dangerous things like cars and medical devices, being produced via provably-correct processes. But that will almost certainly wholly exhaust humanity's reserves of strongly math-educated software engineers (not to mention, industry's willingness to pay for it.) Software engineering may be impossible because most humans don't like math.