Benjamin Pierce interviewed about SAFE project a DARPA project which consist of hardware and software system which has proof of corectness for some part of its design. He talk of which kind of assurance one can count about such a system.