Well I did say "in the theorem-proving sense", meaning that the code undergoes formal verification. There are programming languages for which each function is a theorem that is proved at compile time. That's what I meant.

There are some low-level libraries that have already been partially converted to theorem-proved functions for the sake of security.