I think modern software engineering really needs to start banking on provable languages with strong type systems. Instead of hoping and testing with Monte Carlo sims, let's prove an algorithm once as correct and move on from there.
Only very small parts of software can be proven, especially for things like flight control, where the parameter space is huge, and exhaustive search or manual formal proofs are impossible. Not even speaking of the fact that the spec against which one could build a proof is never error-free to begin with.
In my opinion, this last part is the art, figuring out what to do when you tread a new path. A good engineer will find the critical parts, but that relies on as much intuition as process. A really good engineer will find the meta-mistakes in the process.
The decision to "swing it" can be an engineering decision. If I am doing something I did before, and all the parts fit, I can swing it, and forego a tedious process. I have to balance the risk of implementation delays and bugs vs. spending time on simulation and paperwork.
It's also perfectly possible to do everything by the book and still fail, if the process is a bad fit, or you run out of time because you're all caught up in following procedure instead of taking common sense shortcuts.
So either swinging it or doing it by the book can be engineering or idiocy, depending entirely on the situation, and, in retrospect, the outcome.
The JSF software organization uses static analyzers heavily. They are using theorem provers.