describe static vs dynamic const checks

Author: RalfJung

README.md

@@ -21,6 +21,7 @@ which sort of is a virtual machine using `MIR` as "bytecode".
 ## Table of Contents
 
 * [Const Safety](const_safety.md)
+* [Static and dynamic checks](const_checks.md)
 * The three "kinds" of compile-time evaluated data:
   * [Statics](static.md) (`static`, `static mut`)
   * [Constants](const.md) (`const`, array sizes, non-`Copy` array initializers)

const_checks.md

@@ -0,0 +1,29 @@
+# Static and dynamic checks
+
+This repository describes a set of rules that various forms of compile-time evaluated code needs to satisfy.
+The compiler contains two kinds of checks that guard against violations of these rules: static checks and dynamic checks.
+
+## Dynamic checks
+
+Dynamic checks are conceptually very simple: when evaluating the compile-time code, we look at what it does, and if what it does violates the rules, we halt evaluation.
+Thus, a dynamic check generally makes it very clear what is being protected against.
+
+The main disadvantage of dynamic checks is that they can only run when the compile-time code is being evaluated, which is after monomorphization.
+We generally try to avoid post-monomorphization errors as they make for a bad user experience.
+
+[Promotion analysis](promotion.md) also makes little sense dynamically as it is about code transformation.
+All we can do is check after the transformation if the generated code makes sense.
+
+## Static checks
+
+Static checks work by "looking" at the code.
+(This is "static" as in [static analysis](https://en.wikipedia.org/wiki/Static_analysis), not to be confused with Rust's `static` keyword.)
+The idea is to predict what the code will do without actually executing it.
+That means we can even analyze code that we cannot run pre-monomorphization.
+However, static checks are necessarily less precise than dynamic checks (this is the famous halting problem), which means they will reject code that the dynamic checks would accept.
+
+The key property is that the static check is *sound*, which means that everything accepted by the static checks will also be accepted by the dynamic checks.
+It might seem like this makes the dynamic checks unnecessary, but they are still tremendously useful.
+On the one hand, the dynamic checks serve as a safety net for when we have bugs in the static checks (dynamic checks are much easier to get right, typically).
+On the other hand, having the dynamic checks forces us through the helpful exercise of figuring out what the dynamic property we are enforcing actually *is*, which is crucial when we want to adjust the static check to be more precise.
+The dynamic check serves as the "ground truth" that the static check approximates, and we can improve that approximation over time.

static.md

@@ -14,7 +14,8 @@ Statics (`static`, `static mut`) are the simplest kind of compile-time evaluated
 ## `Drop`
 
 The compiler rejects intermediate values (created and discarded during the computation of a static initializer) that implement `Drop`.
-The reason for this is simply that the `Drop` implementation might be non-`const fn`.
+The reason for this is simply that the `Drop` implementation might be non-`const fn`
+(so really, this is just a special case of static initializers not being able to call non-`const` functions).
 This restriction can be lifted once `const impl Drop for Type` (or something similar) is supported.
 
 ```rust