Yesterday I gave a talk at Stanford in Dawson Engler's Advanced Operating Systems class. It was a variation on talks I've given before, but with a bit more about open source project issues and spec design issues. I pushed the meme of the virtuoso spec editor, something I hope will spread. I also talked about the economics of error recovery --- the fact that recovering from malformed input, instead of hard failure, is a competitive advantage for client software so in a competitive market it's sure to develop and you might as well put it in specifications.
Today I've been at the Berkeley OSQ retreat. As usual it's a lot of fun hanging out with Berkeley and Stanford students and faculty, plus people from Microsoft, Intel and IBM, talking about software improvement research. I especially enjoy it because I know this community well from my research background, but I also have a lot to contribute from my experiences in the Mozilla trenches.
One point I keep making is that we are pretty good at finding bugs, but we need to improve the fixing process. One part of that is to work on debugging, hence Chronicle. Another part is to apply software verification techniques to patches --- we do care very much about avoiding regressions, so identifying new bugs that would be introduced by a patch would be extremely useful (more useful than just identifying existing bugs in the tree).
Another interesting observation is that we want to avoid bug fixes that increase complexity, if possible. That often means a bug fix involves restructuring code followed by a small fix, where the goal of the restructuring is to allow the fix to be small. We can factor this into two changes, where the first change should preserve existing behaviour. It would be great if we had good tools for checking the first change ... and that actually seems like a feasible goal, since the problem is quite crisply defined and should often be solvable using local reasoning. It would certainly be nice, as a code reviewer, if cleanup patches came with a proof that they do not change behaviour (or at least a statement that intensive automated analysis had failed to uncover any issues).