[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!