Coding that can't be hacked?

Professor Kathleen Fisher explains how recent developments by DARPA have allowed computer scientists to use mathematical proofs to verify that code—up to 100,000 lines of it at a time—is functionally correct and free of bugs.
A close up of a computer screen with code on it.