> Are you satisfied like "proof is left as an exercise for the reader" in a math textbook? Or is it like "I have proved this but it's too large to fit in the margins"?
In the first example the proof would be available elsewhere. In the second example, no. My answer is "just the facts as they exist today."
A mathematical proof holds no inherent utility. The thing it proves is what is useful. What I find useful is not suffering memory safety woes. Can I run a tool, any tool, today that will give me the same assurances that the Rust compiler (and/or Miri) does? Conjecture about the future is pointless because someone could equally go and write some static analysis tool like clr for Rust to fix all the bad parts, or fix the compiler, or the parts of clr that aren't finished might be impossible (we don't know, nobody has tried), or the heat death of the universe could come early. All still irrelevant, because I'm a user and I care exclusively about what I can currently do.
In the first example the proof would be available elsewhere. In the second example, no. My answer is "just the facts as they exist today."
A mathematical proof holds no inherent utility. The thing it proves is what is useful. What I find useful is not suffering memory safety woes. Can I run a tool, any tool, today that will give me the same assurances that the Rust compiler (and/or Miri) does? Conjecture about the future is pointless because someone could equally go and write some static analysis tool like clr for Rust to fix all the bad parts, or fix the compiler, or the parts of clr that aren't finished might be impossible (we don't know, nobody has tried), or the heat death of the universe could come early. All still irrelevant, because I'm a user and I care exclusively about what I can currently do.