3 ms·

So, one question might be whether it's possible to encode some of these implicit invariants into the type so that the "evil" function would actually fail to com

So, one question might be whether it's possible to encode some of these implicit invariants into the type so that the "evil" function would actually fail to compile.

Animats 11y ago
That's quite possible, and most proof of correctness systems can do it, but there's no syntax in Rust for talking about the necessary object invariants. Object invariants are assertions which must be true whenever control is not within the object. The object invariants must be true when control leaves the object by exiting any public function. Nothing outside the object must be able to alter the variables involved in the object invariant. Only one execution thread can be in the object at a time. If you can demonstrate all of those conditions, assuming the invariant is true at entry to the object, you have proved the object invariant. This is a useful and well-understood concept in the proof world, but isn't seen much in programming languages.
- ralfj 11y ago
  Since Rust supports concurrency, it is worth mentioning that these techniques have been scaled to handle objects that can be accessed from multiple threads at once - while maintaining the modularity of the approach. See, for example, <http://plv.mpi-sws.org/iris/> http://plv.mpi-sws.org/iris/> and <http://software.imdea.org/fcsl/> http://software.imdea.org/fcsl/>.
gsg 11y ago
Dependent types allow for this kind of thing. Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.
jeffdavis 11y ago
Has anyone discussed adding ada-style contracts to rust?

So, one question might be whether it's possible to encode some of these implicit invariants into the type so that the "evil" function would actually fail to compile.

Animats 11y ago

That's quite possible, and most proof of correctness systems can do it, but there's no syntax in Rust for talking about the necessary object invariants. Object invariants are assertions which must be true whenever control is not within the object. The object invariants must be true when control leaves the object by exiting any public function. Nothing outside the object must be able to alter the variables involved in the object invariant. Only one execution thread can be in the object at a time. If you can demonstrate all of those conditions, assuming the invariant is true at entry to the object, you have proved the object invariant. This is a useful and well-understood concept in the proof world, but isn't seen much in programming languages.

ralfj 11y ago
Since Rust supports concurrency, it is worth mentioning that these techniques have been scaled to handle objects that can be accessed from multiple threads at once - while maintaining the modularity of the approach. See, for example, <http://plv.mpi-sws.org/iris/> http://plv.mpi-sws.org/iris/> and <http://software.imdea.org/fcsl/> http://software.imdea.org/fcsl/>.

gsg 11y ago

Dependent types allow for this kind of thing. Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.

jeffdavis 11y ago

Has anyone discussed adding ada-style contracts to rust?