[cangencer]

The article is extremely shallow beyond saying "Formal verification a la SPARK" should have been used, while not offering how this could actually work in the real world - I don't think the author has any experience working on any similar piece of software either.

While such techniques are available, would they be really applicable in a very dynamic environment such as with millions of PCs running various windows versions, needing continuous / real-time updates.

And yes, we of course know that QA and testing magically removes all possible failure modes/bugs.

[b-man]

> While such techniques are available, would they be really applicable in a very dynamic environment such as with millions of PCs running various windows versions, needing continuous / real-time updates.

I don't see much difference in complexity between the affected software and the several existing formally verified software. At the very least the parser/interpreter could very much be formally verified.

But my point is, have they tried? They don't seem to be even aware of such.