3 ms·
Can your friend prove the Haskell and ML compilers he is using are 100% bug free as well? And the hardware it is running on? (both the compiler and the execut
by thalur 14y ago
Can your friend prove the Haskell and ML compilers he is using are 100% bug free as well? And the hardware it is running on? (both the compiler and the execution environment if they differ)
- oggy 14y agoIf you're interested, the German Verisoft project [1] aims at such pervasive verification. AFAIK they haven't yet verified anything matching the complexity of seL4, but they did verify a simple real-time OS. Of course you do need to stop somewhere, as in trusting something "blindly" (say, the verification tools themselves and the hardware they run on). [1] http://www.ertos.nicta.com.au/publications/papers/Klein_08.pdf http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...