A year or two ago, I worked out a way to compute memory alignment restrictions for data types in C/C++. It's a macro/template trick, which is definitely the sort of thing that should make you wary in general. However, it's turned out to be really useful, and I've never seen a better way to get the same effect.
Every person I've shown the trick to has felt a vague sense of unease. “I don't think I'd trust that. Will that work in all cases?” Even compiler guys have said this.
Well, recently I worked out a proof that it really does work in all cases. Well, “all cases” being “all cases that do not involve a blatantly buggy compiler”. I worked out exactly what I'm requiring of the compiler, and it's not much. This proof makes me worry less about using the trick in real code.
Mostly for my own edification, I've written a little paper about the technique. I'd love to get people's input, either about the technique itself or the way I've explained it in the paper. If anybody's seen the trick before, let me know.
And if any of you know some compiler guys or language nuts, send it their way and ask if they buy my argument.
Here's the paper: http://www.monkeyspeak.com/alignment/