4 ms·
Extrapolating the effort involved in proving huge numbers of complex safety properties for an operating system written in C to programs in general is a bit sill
by gdp 17y ago
Extrapolating the effort involved in proving huge numbers of complex safety properties for an operating system written in C to programs in general is a bit silly. Doing formal verification in more abstract languages gets considerably easier, and considerably easier to mechanise large chunks of the work (a Hindley-Milner type system is a kind of proof of a safety property, for example, and that's totally mechanical).
So it might take 200,000 years to verify Windows, but considerably less to verify an equivalent amount of non-operating system Haskell code, for example.
- billswift 17y agoThe language specification and the compiler would have to be proven correct first. Which is increasingly difficult with higher level languages and with optimizing compilers. The critical aspect is that the MACHINE CODE has to be correct. That is one of the reasons the problem is so hard.
- gdp 17y agoFor this project, that's assumed. Provided you have some kind of formal semantics, you can define translations. And in fact, Adam Chlipala's work on certified compilers show that it's not impossible. http://adam.chlipala.net/papers/CtpcPLDI07/ http://adam.chlipala.net/papers/CtpcPLDI07/ (there are subsequent papers too, but that's probably a good place to start).