Comment by andai

Let me try wrap my head around this.

I notice two classes of bugs in my own programs:

- I meant the code to do X, but it does Y

- I meant the code to do X, and it does X, but X causes problems I didn't foresee

A proof assistant can help you prove the code does X, but it can't help you prove doing X doesn't cause problems you didn't foresee.

In other words, it can prove the soundness of the implementation, but not the design?

Is that right? Though I imagine if there are internal contradictions in the design, lean would catch those too.

So the issue would be "internally consistent yet incorrect designs"?

In the case of TFA, the issue was exhaustiveness, right? "What happens if..."

That sounds like a pretty important quality as far as security goes. Is there a way to make sure everything is actually verified?

I heard actually verifying everything is prohibitively expensive though, like it took 10-20 years to verify seL4 (10K LoC).