describe static vs dynamic const checks

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,32 @@
+# 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 inherently make for a bad user experience.
+While there are technical aspects that could be improved here, the main problem is that the site where the error is reported is disconnected from the site where the root cause is.
+Such problems can be observed when creating an associated constant that uses associated constants from generic parameters.
+These generic parameters are unknown, so the usage of these associated constants may cause errors depending on the *value* of the generic parameter's associated constants.
+
+[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