future work

[web.git] / ralf / _posts / 2017-07-17-types-as-contracts.md

diff --git a/ralf/_posts/2017-07-17-types-as-contracts.md b/ralf/_posts/2017-07-17-types-as-contracts.md
index d11e77b91a0c7dcc751df1e475234fcf0cc2ca80..2d5e3c484218d462ea9df592e453d844018bf269 100644 (file)
--- a/ralf/_posts/2017-07-17-types-as-contracts.md
+++ b/ralf/_posts/2017-07-17-types-as-contracts.md
@@ -366,7 +366,6 @@ One potential middle-ground here is having a function attribute that controls wh
 I have described a mechanism to validate the contract expressed by Rust's types, in particular, the uniqueness and read-only guarantees provided by reference types.
 This validation describes what (safe) code can assume about its variables at run-time, and it enables some code motion optimizations that would otherwise require whole-program alias analysis.
 
 I have described a mechanism to validate the contract expressed by Rust's types, in particular, the uniqueness and read-only guarantees provided by reference types.
 This validation describes what (safe) code can assume about its variables at run-time, and it enables some code motion optimizations that would otherwise require whole-program alias analysis.
 

-

 I said before that I think providing a way to *detect* UB is crucial, and the framework laid out above is designed with this in mind.
 In fact, I have been working on a miri-based implementation of this mechanism:
 [This rustc branch](https://github.com/RalfJung/rust/tree/mir-validate) adds the new `Validate` statement to MIR and adds a MIR pass to insert validation statements as described above, while [this miri branch](https://github.com/RalfJung/miri/tree/mir-validate) adds memory locks to miri and implements type-based validation.
 I said before that I think providing a way to *detect* UB is crucial, and the framework laid out above is designed with this in mind.
 In fact, I have been working on a miri-based implementation of this mechanism:
 [This rustc branch](https://github.com/RalfJung/rust/tree/mir-validate) adds the new `Validate` statement to MIR and adds a MIR pass to insert validation statements as described above, while [this miri branch](https://github.com/RalfJung/miri/tree/mir-validate) adds memory locks to miri and implements type-based validation.


@@ -396,7 +395,11 @@ You have reached the end of this blog post.
 Thanks a lot for reading.
 If you have any comments, please raise them -- the entire purpose of this post is to get the proposal out there so that we can see if this approach can suit the needs of Rust programmers and compiler writers alike.
 If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly or add a note in the [forum](https://internals.rust-lang.org/t/types-as-contracts/5562) for any ammendments that turned out to be necessary.
 Thanks a lot for reading.
 If you have any comments, please raise them -- the entire purpose of this post is to get the proposal out there so that we can see if this approach can suit the needs of Rust programmers and compiler writers alike.
 If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly or add a note in the [forum](https://internals.rust-lang.org/t/types-as-contracts/5562) for any ammendments that turned out to be necessary.

-The concrete proposal will sure need some fixing here and there, but my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
+The concrete proposal will sure need some fixing here and there.
+It is also not complete yet.
+I already mentioned that there are open questions around unsafe code.
+Other areas of future work include `static` variables and the `NonZero` type.
+Nevertheless, my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.

 So, keep the comments flowing -- and safe hacking.
 
 #### Footnotes
 So, keep the comments flowing -- and safe hacking.
 
 #### Footnotes