> meaningful complexity
Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....
> It is not possible to remove ub from the spec
did not say "it is not standard to remove ub"...
Not a part of GP's assertion
> and how many people can check the proofs?
it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion:
> Static analysis tooling has demonstrated that it isn’t up to the task
What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter...
In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed?
I also don’t believe that a single person on the planet can write a secure c program of meaningful complexity. Static analysis tooling has demonstrated that it isn’t up to the task of saving developers from themselves.