[NewsaHackO]

>I think it's ambiguous and fair game for the idea of answering the question "if we write programs in this manner, will there be exploitable bugs?

You're strawmanning the original authors' argument. The creator of lean-zip said that they proved there are no implementation bugs in the lean-zip program. A bug in lean-runtime does not contradict this claim.

[aidenn0]

I'm saying that both the headline of TFA and the statement of the lean-zip creator can be correct.

If they e.g. specially crafted a .zip file that caused it to flip bits via row-hammer like memory accesses, the same would be true.