Really interesting to see progress on the provable correctness and security of software. Pages 11-12 state there is always an inevitable gap between the formal methods and the real world, but this nevertheless sounds a lot better than the hand-wavy, buggy C that gets written today.