OpenBSD and proven secure
"I want to point out that "provably secure" has a specific definition which refers to formal verification through the use of mathematical proofs"
https://www.quora.com/Can-computer-p...rovably-secure
a) Should OpenBSD base program take aim to be written in such a manner that they can be mathematically proven, like seL4?
b) If so is C the language for the further for OpenBSD, or are more complex compilers/languages like Rust needed to improve code correction to a level where it can be mathematically somewhat proven?
I am no dev. Just want to learn.