Earlier quoted context omitted.
The goal of probably secure computing would be merely to (hopefully) extend the mathematical certainties of cryptography to computers and software. The politics of cryptography wouldn’t change, they would only be broadened. Intentional back doors would still be possible, and the ramifications of building them would be just as dire. So the best provable security could do would be to eliminate security holes like buffe…
Then you're probably using the wrong language.
There are some low-level libraries that have already been partially converted to theorem-proved functions for the sake of security.