3 ms·

Does the proof encompass some sort of proof of amount of RAM consumption in it, presumably bounded by some characteristic of the problem presented? Regardless,

by jerf 4y ago

Does the proof encompass some sort of proof of amount of RAM consumption in it, presumably bounded by some characteristic of the problem presented? Regardless, this is very impressive, and one of the first things to raise my eyebrows w.r.t. formal proofs being possibly useful in the real world in a long time. If safe Rust can function as the bridge between the "practical" world and the world of proofs, that alone would be enough to justify Rust's existence.

Jweb_Guru 4y ago
No, it does not. This is mentioned as a limitation in the paper (it does, however, handle things like integer overflows correctly). I believe with some suitable extensions, it would be possible to prove invariants like this as well, but IMO functional correctness is a pretty good start!
Sarek 4y ago
It does assume enough RAM, as it has no way of knowing how much RAM the target machine will have. It is thus correct with regards to the model specified by Rust, but a program which is proven correct in Creusot may get an OOM-error. A note here is that it will not provide the wrong answer due to insufficient memory, but it will crash. Proving some upper bound on the amount of memory used (and potentially gracefully exiting) should be possible, but I have not prioritised it, as OOM has not been an issue.
- jerf 4y ago
  "has no way of knowing how much RAM the target machine will have" That's why I phrased it in terms of a bound based on some characteristic of the problem. But I was just asking for information. I know it's a well-known problem. To be honest the fact that we're even seriously discussing this as something that may be doable is a huge step forward. AIUI, previous state of the art on real languages would have this as hopelessly pie-in-the-sky. I think in many cases memory bound is uninteresting; one could examine a vector implementation and be satisfied that it won't explode unnecessarily. After all, we do exactly that on non-proved implementations without too much fear all the time. SAT just came to mind as a problem where that could be an interesting thing to be able to prove.
viccuad 4y ago
That's analogous to the halting problem.

by jerf 4y ago

Jweb_Guru 4y ago

No, it does not. This is mentioned as a limitation in the paper (it does, however, handle things like integer overflows correctly). I believe with some suitable extensions, it would be possible to prove invariants like this as well, but IMO functional correctness is a pretty good start!

Sarek 4y ago

It does assume enough RAM, as it has no way of knowing how much RAM the target machine will have. It is thus correct with regards to the model specified by Rust, but a program which is proven correct in Creusot may get an OOM-error. A note here is that it will not provide the wrong answer due to insufficient memory, but it will crash. Proving some upper bound on the amount of memory used (and potentially gracefully exiting) should be possible, but I have not prioritised it, as OOM has not been an issue.

jerf 4y ago
"has no way of knowing how much RAM the target machine will have" That's why I phrased it in terms of a bound based on some characteristic of the problem. But I was just asking for information. I know it's a well-known problem. To be honest the fact that we're even seriously discussing this as something that may be doable is a huge step forward. AIUI, previous state of the art on real languages would have this as hopelessly pie-in-the-sky. I think in many cases memory bound is uninteresting; one could examine a vector implementation and be satisfied that it won't explode unnecessarily. After all, we do exactly that on non-proved implementations without too much fear all the time. SAT just came to mind as a problem where that could be an interesting thing to be able to prove.

viccuad 4y ago

That's analogous to the halting problem.