But, if you don't even try to prove part of a process correct, it's almost certainly wrong. See the excellent work that John Regehr's group is doing related to

But, if you don't even try to prove part of a process correct, it's almost certainly wrong. See the excellent work that John Regehr's group is doing related to compiler and optimization verification/testing (http://www.cs.utah.edu/~regehr/research/ http://www.cs.utah.edu/~regehr/research/ ), much of which has been talked about here. There are other folks who have successfully done formal verification of operating systems, device drivers, hardware design, etc. It's a big, hard problem, but we'll get to the "whole stack" eventually.