I have heard from someone involved with project management of military aircraft software that the process includes verification of machine code produced by the compiler, that is: you have to prove that the code generated is exactly what you intended to get.

http://www.sandroid.org/birdsproject/4dummies.html gives a glimpse of how much fun developing software for aviation purposes is.

Computer hardware is not correct. So, you need to step past mathematical perfection and write defensively.

Rule 1: you can't trust RAM it lies.

That said you can build automated tests that add random memory errors to help find the program that's best able to handle memory errors.

I have never seen a piece of software that is built with memory error tolerance is tested against random memory errors. Have you?

Maybe a spacecraft might have some. Error correcting memory, and the software associated with it is, of course, an exception. Is there code dealing with memory errors somewhere in the kernel (of any OS)?

For most programming, it would simply not make sense to try to take memory errors into account. It's very unlikely that in the lifetime of the program, there will ever be a situation where a bit will be flipped and it will have an actual effect.

They are a lot more common than you might think, basicly every day every PC has a memory error. If one of the textures in a video game gets corrupted you may not notice it, and if you have real issues simply rebooting tends to work well. Recent tests give widely varying error rates with over 7 orders of magnitude difference, ranging from 10^−10 to 10^17 error/bit·h, roughly one bit error, per hour, per gigabyte of memory to one bit error, per century, per gigabyte of memory.[7][8][9] http://en.wikipedia.org/wiki/Dynamic_random-access_memory The biggest defence for a home user is simply the banial nature of most information stored in memory.

Yet, you don't have to be building a spacecraft for rebooting to be an issue. One example that comes to mind is remote sensors. A friend was working on power meter which reported back it's findings every few days. The initial version used normal programming practices and after a six months field test of a few thousand units the projected failure rate over 10 years in the field was unacceptably high. He said the code was simple and 'correct' but failed to deal with with corruption. His version had less than 1% of the original failure rate in the field and is projected to save the company far more than his 6 month contract to rewrite the thing from scratch.

A more dramatic example is your car's internal engine controls. But, there they simply reboot regularly as there is no need for maintaining state over the long term.

You too might be intressted in the link I posted above. Its about building safe hardware (and software), but I don't think its completly safe to anykind of random bit-flips.

What you are talking about is the "trusted computing base". Prove every part of the basesystem your running on, this of course is a HUGE task, but there are people thinking and working on this.

You might injoy this darpa project: http://www.crash-safe.org/papers

The propose there own hardware, OS, languages and compilers. The Hardware Design is by Tom Knight, one of the guys who designed the lisp machine.

Its quite an intressting read.