Side note: Nothing is provable in rust because it does not have a formal, verifiable specification. We have a reference implementation that we believe does the things it says it does on one particular architecture. But trust, not proofs, is indeed required. >:) (don't downvote murder me, I love rust)