Add doc/note/assertions.md
diff --git a/doc/note/assertions.md b/doc/note/assertions.md
new file mode 100644
index 0000000..00df4ff
--- /dev/null
+++ b/doc/note/assertions.md
@@ -0,0 +1,83 @@
+# Assertions
+
+Assertions are statements that introduce new compile-time
+[facts](/doc/note/facts.md). They are not comments, as removing them can
+prevent the code from compiling, but unlike other programming languages, Wuffs'
+assertions have no run-time effect at all, not even in a "debug, not release"
+configuration. Compiling an assert will fail unless it can be proven.
+
+The basic form is `assert some_boolean_expression`, which creates
+`some_boolean_expression` as a fact. That expression must be free of
+side-effects: any function calls within must be [pure](/doc/note/effects.md).
+
+Arithmetic inside assertions is performed in ideal integer math, working in the
+integer ring ℤ. An expression like `x + y` in an assertion never overflows,
+even if `x` and `y` have a realized (non-ideal) integer type like `u32`.
+
+Some assertions can be proven by the compiler with no further guidance. For
+example, if `x == 1` is already a fact, then `x < 5` can be automatically
+proved. Adding a seemingly redundant fact can be useful when reconciling
+multiple arms of an if-else chain, as
+[reconciliation](/doc/note/facts.md#situations-and-reconciliation) requires the
+facts in each arm's final situation to match exactly:
+
+```
+if x < 5 {
+ // No further action is required. "x < 5" is a fact in the 'if' arm.
+
+} else {
+ x = 1
+ // At this point, "x == 1" is a fact, but "x < 5" is not.
+
+ // This assertion creates the "x < 5" fact.
+ assert x < 5
+}
+
+// Here, "x < 5" is still a fact, since the exact boolean expression "x < 5"
+// was a fact at the end of every arm of the if-else chain.
+```
+
+TODO: specify what can be proved automatically, without naming an axiom.
+
+
+## Axioms
+
+Wuffs' assertion system is a proof checker, not an SMT solver or automated
+theorem prover. It verifies explicit proof targets instead of the more
+open-ended task of searching for implicit ones. This involves more explicit
+work by the programmer, but compile times matter, so the Wuffs compiler is fast
+(and dumb) instead of smart (and slow).
+
+The Wuffs syntax is regular (and unlike C++, does not require a symbol table to
+parse), so it should be straightforward to transform Wuffs code to and from
+file formats used by more sophisticated proof engines. Nonetheless, that is out
+of scope of this respository and the Wuffs compiler per se.
+
+Again for compilation speed, not every inference rule is applied after every
+line of code. Some assertions require explicit guidance, naming the rule that
+proves the assertion. These names are simply strings that resemble mathematical
+statements. They are axiomatic, in that these rules are assumed, not proved, by
+the Wuffs toolchain. They are typically at a higher level than e.g. Peano
+axioms, as Wuffs emphasizes practicality over theoretical minimalism. As they
+are axiomatic, they endeavour to only encode 'obvious' mathematical rules.
+
+For example, the axiom named `"a < b: a < c; c <= b"` is about transitivity:
+the assertion `a < b` is proved if both `a < c` and `c <= b` are true, for some
+(pure) expression `c`. Terms like `a`, `b` and `c` here are all integers in ℤ,
+they do not encompass floating point concepts like negative zero, `NaN`s or
+rounding. The axiom is invoked by extending an `assert` with the `via` keyword:
+
+```
+assert n_bits < 12 via "a < b: a < c; c <= b"(c: width)
+```
+
+This proves `n_bits < 12` by applying that transitivity axiom, where `a` is
+`n_bits`, `b` is `12` and `c` is `width`. Compiling this assertion requires
+proving both `n_bits < width` and `width <= 12`, from existing facts or from
+the type system, e.g. `width` is a `base.u32[..= 12]`.
+
+The trailing `(c: width)` syntax is deliberately similar to a function call
+(recall that when calling a Wuffs function, each argument must be named), but
+the `"a < b: a < c; c <= b"` named axiom is not a function-typed expression.
+
+The [compiler's built-in axioms](/lang/check/axioms.md) are listed separately.
diff --git a/lang/check/axioms.md b/lang/check/axioms.md
index 829884e..26efcd5 100644
--- a/lang/check/axioms.md
+++ b/lang/check/axioms.md
@@ -1,17 +1,12 @@
-# Axioms
+# Axiom Listing
-This file lists Wuffs' axioms: a fixed list of built-in, self-evident rules to
-combine existing facts to create new facts. For example, given numerical-typed
-expressions `a`, `b` and `c`, the two facts that `a < c` and `c <= b` together
-imply that `a < b`: less-than-ness is transitive.
+This file lists Wuffs' [axioms](/doc/note/assertions.md#axioms): a fixed list
+of built-in, self-evident rules to create new facts by combining existing
+facts. For example, given numerical-typed expressions `a`, `b` and `c`, the two
+facts that `a < c` and `c <= b` together imply that `a < b`: less-than-ness is
+transitive. That rule is named by the string "a < b: a < c; c <= b"`.
-Wuffs code represents this axiom by the string `"a < b: a < c; c <= b"`, and it
-is invoked by the `assert` and `via` keywords, naming the rule and [binding the
-expressions `a`, `b` and
-`c`](https://github.com/google/wuffs/blob/4080840928c0b05a80cda0d14ac2e2615f679f1a/std/lzw/decode_lzw.wuffs#L99).
-
-This file is not just documentation. It is
-[parsed](https://github.com/google/wuffs/blob/master/lang/check/gen.go) to give
+This file is not just documentation. It is [parsed](/lang/check/gen.go) to give
the list of axioms built into the Wuffs compiler. Run `go generate` after
editing this list.
