more https

[web.git] / personal / _posts / 2018-07-19-const.md

diff --git a/personal/_posts/2018-07-19-const.md b/personal/_posts/2018-07-19-const.md
index d523935c8030bcb6ea4e55a1a6f6e795be0a76d2..a2f95525f01afd20a438b5861acefc5717cd4fc8 100644 (file)
--- a/personal/_posts/2018-07-19-const.md
+++ b/personal/_posts/2018-07-19-const.md
@@ -13,18 +13,18 @@ Expect something like a structured brain dump, so there are some unanswered ques
 
 ## Some Background
 
 
 ## Some Background
 

-CTFE is the mechanism used by the compiler, primarily, to evaluate items like `const x : T = ...;`.
+CTFE is the mechanism used by the compiler, primarily, to evaluate items like `const x: T = ...;`.

 The `...` here is going to be Rust code that must be "run" at compile-time, because it can be used as a constant in the code -- for example, it can be used for array lengths.
 
 The `...` here is going to be Rust code that must be "run" at compile-time, because it can be used as a constant in the code -- for example, it can be used for array lengths.
 

-Notice that CTFE is *not* the same as constant propagation: Constant propagation is an optimization pass done by LLVM that will opportunistically change code like `3 + 4` into `7` to avoid run-time work.
+Notice that CTFE is *not* the same as constant propagation: Constant propagation is an optimization pass done by compilers like LLVM that will opportunistically change code like `3 + 4` into `7` to avoid run-time work.

 Being an optimization, constant propagation must, by definition, not change program behavior and will not be observable at all (other than performance).
 CTFE, on the other hand, is about code that *must* be executed at compile-time because the compiler needs to know its result to proceed -- for example, it needs to know the size of an array to compute how to lay out data in memory.
 You can statically see, just from the syntax of the code, whether CTFE applies to some piece of code or not:
 CTFE is only used in places like the value of a `const` or the length of an array.
 {% highlight rust %}
 fn demo() {
 Being an optimization, constant propagation must, by definition, not change program behavior and will not be observable at all (other than performance).
 CTFE, on the other hand, is about code that *must* be executed at compile-time because the compiler needs to know its result to proceed -- for example, it needs to know the size of an array to compute how to lay out data in memory.
 You can statically see, just from the syntax of the code, whether CTFE applies to some piece of code or not:
 CTFE is only used in places like the value of a `const` or the length of an array.
 {% highlight rust %}
 fn demo() {

-  const X : u32 = 3 + 4; // CTFE
-  let x : u32 = 4 + 3; // no CTFE (but maybe constant propagation)
+  const X: u32 = 3 + 4; // CTFE
+  let x: u32 = 4 + 3; // no CTFE (but maybe constant propagation)

 }
 {% endhighlight %}
 We say that the `3 + 4` above is in *const context* and hence subject to CTFE, but the `4 + 3` is not.
 }
 {% endhighlight %}
 We say that the `3 + 4` above is in *const context* and hence subject to CTFE, but the `4 + 3` is not.


@@ -33,9 +33,13 @@ We say that the `3 + 4` above is in *const context* and hence subject to CTFE, b
 
 Not all operations can be used in const context.
 For example, it makes no sense to compute your array length as "please go read that file from disk and compute something" -- we can't know what will be on the disk when the program actually runs.
 
 Not all operations can be used in const context.
 For example, it makes no sense to compute your array length as "please go read that file from disk and compute something" -- we can't know what will be on the disk when the program actually runs.

-We could use the disk of the machine compiling the program, but that does not sound very appearling either.
-In fact, it would also be grossly unsafe:
+We could use the disk of the machine compiling the program, but that does not sound very appealing either.
+Things get even worse when you consider letting the program send information to the network.
+Clearly, we don't want CTFE to have actually observable side-effects outside of compilation.
+
+In fact, just naively letting programs read files would also be grossly unsafe:

 When computing the length of an array twice, it is important that we obtain the same result.
 When computing the length of an array twice, it is important that we obtain the same result.

+**Update:** As @eddyb points out, things get even worse once you consider const generics, traits, and coherence: At that point, you have to [rely on evaluating the same expression in different crates to produce the same result](https://internals.rust-lang.org/t/mir-constant-evaluation/3143/47). **/Update**

 
 > *CTFE must be deterministic.*
 
 
 > *CTFE must be deterministic.*
 


@@ -135,7 +139,8 @@ So, we will likely have to live with either considering floating point operation
 I think it is possible to achieve CTFE correctness for all other operations, and I think we should strive to do so.
 
 Before we go on, notice that CTFE correctness as defined above does not say anything about the case where CTFE fails with an error, e.g. because of an unsupported operation.
 I think it is possible to achieve CTFE correctness for all other operations, and I think we should strive to do so.
 
 Before we go on, notice that CTFE correctness as defined above does not say anything about the case where CTFE fails with an error, e.g. because of an unsupported operation.

-That is a deliberate choice because it lets us gradually improve the operations supported by CTFE, but it is a choice that not everyone might agree with.
+CTFE would be trivially correct (in the above sense) if it just always immediately returned an error.
+However, since const-safe programs cannot error during CTFE, we know from CTFE correctness that *those* programs *do* in fact behave exactly the same at compile-time and at run-time.

 
 ## Unsafe Blocks in Const Context
 
 
 ## Unsafe Blocks in Const Context
 


@@ -228,8 +233,10 @@ I am not sure which effect that should or will have for promotion.
 ## Conclusion
 
 I have discussed the notions of CTFE determinism and CTFE correctness (which are properties of a CTFE engine like miri), as well as const safety (property of a piece of code) and const soundness (property of a type system).
 ## Conclusion
 
 I have discussed the notions of CTFE determinism and CTFE correctness (which are properties of a CTFE engine like miri), as well as const safety (property of a piece of code) and const soundness (property of a type system).

+In particular, I propose that *when type-checking safe code in const context, we guarantee that this code is const-safe*, i.e., that it will not hit a CTFE error (though panics are allowed, just like they are in "run-time" Rust code).
+

 There are still plenty of open questions, in particular around the interaction of [`const fn` and traits](https://github.com/rust-lang/rust/issues/24111#issuecomment-311029471), but I hope this terminology is useful when having those discussions.
 Let the type systems guide us :)
 
 There are still plenty of open questions, in particular around the interaction of [`const fn` and traits](https://github.com/rust-lang/rust/issues/24111#issuecomment-311029471), but I hope this terminology is useful when having those discussions.
 Let the type systems guide us :)
 

-Thanks to @oli-obk for feedback on a draft of this post.
+Thanks to @oli-obk for feedback on a draft of this post, and to @centril for interesting discussion in #rust-lang that triggered me into developing these ideas and terminology.

 If you have feedback or questions, [let's discuss in the internals forum](https://internals.rust-lang.org/t/thoughts-on-compile-time-function-evaluation-and-type-systems/8004)!
 If you have feedback or questions, [let's discuss in the internals forum](https://internals.rust-lang.org/t/thoughts-on-compile-time-function-evaluation-and-type-systems/8004)!