Anything on theoretical advances in proving programs would be appreciated too (math isn't a problem).
If you're into formal proofs you should be taking a look at things like the Z language. However these systems are a lot less useful than many people imagine. Even with Z the task of proving a program does what you think it does is hard, and the problem of ensuring that your real-world requirements match your Z-code is still non-trivial. All they do is move the problem up a level.
The common problem with all these books I've found is that they lack substance, seeming to focus almost entirely on metaphors and don't provide anything that can be directly applied.
Personally I'd take another look at XP. I'm not sure what books you've been reading, but XP is all about directly applicable rules and practices. Rules and practices that I have found very effective at increasing code quality.
Can anyone shed some light on the practices that allow software to be used in applications where any failure is simply not acceptable? Thank you for your responses.
If you really mean "not acceptable" than it's all about large amounts of requirements tracking, testing and process. For example, see this article on the on-board shuttle group at Lockheed Martin - the people who write the software that runs the space shuttle.
Are you posting in the right place? Check out Where do I post X? to know for sure.
Posts may use any of the Perl Monks Approved HTML tags. Currently these include the following:
<code> <a> <b> <big>
<blockquote> <br /> <dd>
<dl> <dt> <em> <font>
<h1> <h2> <h3> <h4>
<h5> <h6> <hr /> <i>
<li> <nbsp> <ol> <p>
<small> <strike> <strong>
<sub> <sup> <table>
<td> <th> <tr> <tt>
Snippets of code should be wrapped in
<code> tags not
<pre> tags. In fact, <pre>
tags should generally be avoided. If they must
be used, extreme care should be
taken to ensure that their contents do not
have long lines (<70 chars), in order to prevent
horizontal scrolling (and possible janitor
Want more info? How to link or
or How to display code and escape characters
are good places to start.