4 ms·
If you verify the correctness of the CLR, by the same reasoning don't you have to verify the correctness of Windows as well?
by hamidpalo 15y ago
If you verify the correctness of the CLR, by the same reasoning don't you have to verify the correctness of Windows as well?
- DanWaterworth 15y agoYes, 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.
- CurtHagenlocher 15y agoIf you verify the correctness of Windows, don't you have to verify the correctness of all the parts in the hardware stack?