Great video. I remember reading a piece some time ago about militairy software, and proofing correct operation of it. If I remember correctly, they where able to proof the complete application/system, not just the device drivers. Now I wander if maybe
there are programming languages for which it is much easier to find proof of correct functioning that it is for c(++)?