DARPA SEEKS HACK-PROOF COMPUTER CODE: It’s being tested.

…the computer code underpinning the hardware was essentially unhackable with current technology. The report notes the code is “as trustworthy as a mathematical proof.” The programming approach is known as formal verification, and it’s written informally and evaluated based on whether it works or not. The language follows step-by-step, logically, and can be tested just like a mathematical proof. So why is this formal verification essentially hack-proof? Because most hacks are made by exploiting bugs and errors in code. Code that’s gone through this process, with this approach, is supposed to be bug-proof. So there are no holes for hackers to exploit, because the code just works.