[Refefer]

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.

[skywhopper]

More provable code is not the answer. Proving the functionality is meaningless if you can't decide on what the functionality should be. And this project has all the classic hallmarks of a requirements quagmire. The requirements are poorly specified and contradictory, and provable code and strong typing can't solve that problem.

[jerf]

Indeed, it makes the problem worse... the strong typing and provable code stubbornly insist that the requirements are contradictory and refuse to even compile. But managers don't want to hear that, of course, so we go back to the dumber languages that happily compile even so. This does not make the requirements any less contradictory of course... it just means that the dumber languages will let you blithely code on, and are guaranteed to do something stupid at run time instead. Progress!

[mariusz79]

Or in other words - we need to move from art to engineering

[dognotdog]

Engineering is systematic approximations and best-guessing. The art of it is knowing when shortcuts are good enough.

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.

[mariusz79]

And what in your opinion is the difference between "systematic approximations and best-guessig" and "knowing when shortcuts are good enough"? For me engineering is using proven and tested solutions every time, even if the solution is not sexy, and art is just "swinging it" - just like using js for everything when they are better more mature solutions.

[dognotdog]

Since you're not building the same thing every time, you don't have wholesale proven and tested solutions for everything. The engineering part is going about filling the gaps systematically, and figuring out what parts require closer inspection in the first place.

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.

[Daniel_Newby]

A lot of things, like nonlinear control systems, can only be verified by Monte Carlo methods. Subsystem failure tolerance is difficult to handle by any existing theorem prover.

The JSF software organization uses static analyzers heavily. They are using theorem provers.