3 ms·
Yes, I hadn't thought of that. The point is that proving part of a process correct without proving correct the entire stack, is no guarantee that it does anythi
by DanWaterworth 15y ago
Yes, I hadn't thought of that. The point is that proving part of a process correct without proving correct the entire stack, is no guarantee that it does anything like what it's supposed to.
- larsberg 15y agoBut, 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.