[sliverstorm]

in general, trying to prove that the software was going to work right, leaving the engineers with very little time to write the actual software...

Sure sounds like the way it should be to me. Maybe it needs to be made easier to prove your software is correct, but to me it seems like for systems like airplanes, code that cannot be proven correct is worthless.

Considering most programmers are said to produce 6 lines of good code a day, maybe it's not even actually slower in the end if the formal verification process filters out every other line you would have written that day.

[calebm]

It's not a bad thing to put in quality assurance measures in place. It's a bad thing, though, if so much time is spent on QA, that there you are rushing to write the actual code. Rushed coding does not produce quality.