|
|
|
|
|
|
by throwawaymaths
497 days ago
|
|
|
I guess the question is what level of satisfied are you. 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"? It seems author couldn't be bothered to complete it since there's (minor) missing features in the zig compiler that need to be satisfied first to make it worthwhile? |
|
|
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.