> However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Either yo

> However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Either you reasonably need machine-checkable proofs of the software confirming to a spec, or you don't and can settle for less secure methods. Then be honest and lay out what parts of the program are verified, which are proven ~informally by hand, which has been reviewed by several people, which uses a lot of tests, and so on. Risk/reward analysis like anything else (but obviously not straightforward). Formal verification is probably so young/not widespread as a discipline that we'll probably see peanut gallery concern trolling "this is really cool! But... <same old FUD>" like your comments for the next twenty years or so.