From 81ac1ea04b326d52734fbf5a666039c53c52dd28 Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 9 Sep 2025 16:32:08 -0700
Subject: [PATCH 01/12] Some general cleanup and math support

Made a pass fixing spelling, math expressions (added ketex - see README), made indentation more consistent, removed non-ascii characters in favor of entities, and changed links to markdown format so they can be clicked in the generated docs.
---
 .vscode/settings.json                  |   8 +-
 better-code/README.md                  |   3 +-
 better-code/book.toml                  |   3 +
 better-code/src/chapter-2-contracts.md | 134 +++++++++++++------------
 4 files changed, 81 insertions(+), 67 deletions(-)

diff --git a/.vscode/settings.json b/.vscode/settings.json
index c03803f..f746685 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -6,5 +6,11 @@
         }
     ],
     "rewrap.autoWrap.enabled": true,
-    "rewrap.wrappingColumn": 80
+    "rewrap.wrappingColumn": 80,
+    "cSpell.words": [
+        "footgun",
+        "Gitter",
+        "irreflexivity",
+        "preorder"
+    ]
 }
diff --git a/better-code/README.md b/better-code/README.md
index 1125d25..f5c7ff2 100644
--- a/better-code/README.md
+++ b/better-code/README.md
@@ -19,7 +19,8 @@ Download the installer from [here](https://win.rustup.rs/).
 ### Install mdBook
 
 ```bash
-cargo install mdbook
+cargo install mdbook@0.4.48
+cargo install mdbook-katex
 ```
 
 ### Building and Serving the Book
diff --git a/better-code/book.toml b/better-code/book.toml
index 5bd576a..6fab910 100644
--- a/better-code/book.toml
+++ b/better-code/book.toml
@@ -20,3 +20,6 @@ enable = true
 
 [output.html.print]
 enable = true
+
+[preprocessor.katex]
+after = ["links"]
diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index 994886e..ba7f8d6 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -135,26 +135,29 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> {P}S{Q}
+> $\{P\}S\{Q\}$
 
-which is an assertion that if **precondition** *P* is met, operation
-*S* establishes **postcondition** *Q*.
+which is an assertion that if **precondition** $P$ is met, operation
+$S$ establishes **postcondition** $Q$.
+
+<!-- This had been using math for pre and post conditions, but I find mixing math and code makes it look like we are talking about different `x` and $x$ variables and equality vs. assignment gets confusing. I think if the operation is expressed in code, the conditions should be expressed in code. -->
 
 For example:
 
-- if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
+- if we start with $\{$ `x == 2` $\}$ (precondition), after `x += 1`, $\{$ `x == 3` $\}$ (postcondition):
+
+  > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
 
-  > {x == 2}x+=1{x == 3}
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > {x < Int.max}x+=1{x > Int.min}
+  > $\{$`x < Int.max`$\}$ `x += 1` $\{$`x > Int.min`$\}$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> {P}S{Q} ∧ {Q}T{R} ⇒ {P}S;T{R}
+> $\{P\}S\{Q\} \wedge \{Q\}T\{R\} \Rightarrow \{P\}S;T\{R\}$
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing
@@ -176,13 +179,13 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-**{*l*+*m*=0}**`h = l + m`**{*h*≤0}**.  This one isn't particularly
+$\{$ `l + m == 0` $\}$ `h = l + m` $\{$ `h <= 0` $\}$. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- **{*l*≤*h*}**`let m = (h - l )/2`**{*m*≥ 0}**, i.e.
+- $\{$ `l <= h` $\}$ `let m = (h - l )/2` $\{$ `m >= 0` $\}$, i.e.,
 
   ```swift
   // precondition: l <= h
@@ -190,7 +193,7 @@ The following—more useful—triples will help illustrate the sequencing rule:
   // postcondition: m >= 0
   ```
 
-- **{*m*≥0}**`h = l + m`**{*l*≤*h*}**, i.e.
+- $\{$ `m >= 0` $\}$ `h = l + m` $\{$ `l <= h` $\}$, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -203,16 +206,16 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-**{*l*≤*h*}**`let m = (h -l )/2; h = l + m`**{*l*≤*h*}**, i.e.
+$\{$ `l <= h` $\}$ `let m = (h - l) / 2; h = l + m` $\{$ `l <= h` $\}$, i.e.,
 
 ```swift
-  // precondition: l <= h
-  let m = (h - l) / 2
-  h = l + m
-  // postcondition: l <= h
+// precondition: l <= h
+let m = (h - l) / 2
+h = l + m
+// postcondition: l <= h
 ```
 
-which says that if *l*≤*h* is true on entry to the sequence, it is
+which says that if `l <= h` is true on entry to the sequence, it is
 also true on exit.
 
 ### Invariants
@@ -251,12 +254,12 @@ step in understanding what it does.
 
 ## Design By Contract
 
-> *…a software system is viewed as a set of communicating components
+> *&hellip;a software system is viewed as a set of communicating components
 > whose interaction is based on precisely defined specifications of
-> the mutual obligations — contracts.*
+> the mutual obligations &ndash; contracts.*
 >
->   —Building bug-free O-O software: An Introduction to Design by Contract™
->    https://www.eiffel.com/values/design-by-contract/introduction/
+>   &mdash; Building bug-free O-O software: An Introduction to Design by Contract&trade;
+>    <https://www.eiffel.com/values/design-by-contract/introduction/>
 
 In the mid 1980s, The French computer scientist Bertrand Meyer took
 Hoare Logic, and shaped it into a practical discipline for software
@@ -293,10 +296,10 @@ When something goes wrong in software, focusing on which *person* to
 blame is counterproductive, but deciding which *code* is to blame is
 the first step.  Contracts tell us which code needs fixing:
 
-- If preconditions aren't satisifed, that's a bug in the caller.  The
+- If preconditions aren't satisfied, that's a bug in the caller.  The
   function is not required to make any promises[^no-promises] in that case.
 
-- If preconditions are statisfied but postconditions are not
+- If preconditions are satisfied but postconditions are not
   fulfilled, that's a bug in the callee, or in something it calls.
 
 [^no-promises]: In fact, a function *shouldn't* make any promises in
@@ -324,7 +327,7 @@ When we talk about an instance being “in a good state,” we
 mean that its type's invariants are satisfied.
 
 For example, this type's public interface is like an
-array of pairs, but it stores elements of those pairs separate
+array of pairs, but it stores elements of those pairs in separate
 arrays.[^array-pairs]
 
 [^array-pairs]: You might want to use a type like this one to store
@@ -364,7 +367,7 @@ struct PairArray<X, Y> {
 The invariant for this type is that the private arrays have the same
 length.  It's important to remember that invariants only hold at a
 type's public interface boundary and are routinely violated,
-temporarily, durign a mutation.  For example, in `append`, we have to
+temporarily, during a mutation.  For example, in `append`, we have to
 grow one of the arrays first, which breaks the invariant until we've
 done the second `append`.  That's not a problem because the arrays are
 private—that “bad” state is *encapsulated* by the type, and
@@ -479,7 +482,7 @@ neither correct nor incorrect; it does something, but does it do the
 
 > All undocumented software is waste. It's a liability for a company.
 >
-> —Alexander Stepanov (https://youtu.be/COuHLky7E2Q?t=1773)
+> &mdash; Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>)
 
 
 Documentation is also essential for local reasoning.  We build atop
@@ -699,7 +702,7 @@ implementation, and should be encoded in ordinary comments addressed
 privately to the maintainer of the code.  Note that you
 can have both: `PairArray` *also* has a public invariant that its
 `count` is non-negative.  We'll get to why this particular invariant
-is not explicitlty documented in a moment…
+is not explicitly documented in a moment…
 
 ### Making It Tractable
 
@@ -712,7 +715,7 @@ Now, not every contract is as simple as the ones we've shown so far,
 but simplicity is a goal.  In fact, if you can't write a terse,
 simple, but _complete_ contract for a component, there's a good chance
 it's badly designed.  A classic example is the C library `realloc`
-function, which does at least three different things—allocate, deallocate, and resize 
+function, which does at least three different things—allocate, deallocate, and resize
 dynamic memory—all of which
 need to be described. A better design would have separated these
 functions.  So simple contracts are both easy to digest and easy to
@@ -822,7 +825,7 @@ part of the method*.
   /// - Precondition: `self` is non-empty.
   /// - Postcondition: The length is one less than before
   ///   the call. Returns the original last element.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 The invariant of this function is the rest of the elements, which are
@@ -835,7 +838,7 @@ unchanged:
   /// - Postcondition: The length is one less than before
   ///   the call. Returns the original last element.
   /// - Invariant: the values of the remaining elements.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 Now, if the postcondition seems a bit glaringly redundant with the
@@ -865,7 +868,7 @@ omitted.
   /// Removes and returns the last element.
   ///
   /// - Precondition: `self` is non-empty.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 In fact, the precondition is implied by the summary too.  You
@@ -884,7 +887,7 @@ should be sufficient:
 
 ```swift
   /// Removes and returns the last element.
- public mutating func popLast() -> T { ... }
+  public mutating func popLast() -> T { ... }
 ```
 
 In practice, once you are comfortable with this discipline, the
@@ -926,6 +929,8 @@ the elements arranged from least to greatest. The contract gives an
 explicit precondition that isn't implied by the summary: it requires
 that the predicate be a strict weak ordering.
 
+<!-- SRP: this section bothers me. "among others" instead of fully spelling out the requirements, using (i, j + 1) which may not exist, and the n^2 comparisons without calling out the O(n^3) complexity or which properties could be practically checked. Also is "stable" the term we want to use? Regular and deterministic are also candidates. I've tried to rewrite this a couple of times, but it just gets too complex and the main point is lost. -->
+
 _Some_ precondition on the predicate is needed just to make the result
 a meaningful sort with respect to the predicate.  For example, a
 totally unconstrained predicate could return random boolean values,
@@ -933,7 +938,7 @@ and there's no reasonable sense in which the function could be said to
 leave the elements sorted with respect to that.  Therefore the
 predicate at least has to be stable. To leave elements meaningfully
 sorted, the predicate has to be *transitive*: if it is `true` for
-elements (*i*, *j*), it must also be true for elements (*i*, *j*+1).
+elements $(i, j)$, it must also be true for elements $(i, j + 1)$.
 A strict weak ordering has both of these properties, among others.
 
 Note that the performance of this method is documented.  Time and
@@ -944,8 +949,9 @@ function as part of its postconditions, which brings all the
 function's guarantees under one name: its postconditions.
 
 The strict weak ordering requirement is a great example of a
-precondition that can't be efficiently checked.  To do so would
-require at least *N*² comparisons, where *N* is the number of
+precondition that can't be efficiently checked.  Even if we could assume the
+comparison is stable, to do so would
+require at least $n^2$ comparisons, where $n$ is the number of
 elements, which would violate the complexity bound of the algorithm.
 
 The summary gives the postcondition that no two adjacent elements are
@@ -967,9 +973,9 @@ understood, is another source of complexity. In fact we should
 probably put a link in the documentation to a definition.
 
 ```swift
-/// - Precondition: `areInIncreasingOrder` is [a strict weak
-///   ordering](https://simple.wikipedia.org/wiki/Strict_weak_ordering)
-///   over the elements of `self`.
+  /// - Precondition: `areInIncreasingOrder` is [a strict weak
+  ///   ordering](https://simple.wikipedia.org/wiki/Strict_weak_ordering)
+  ///   over the elements of `self`.
 ```
 
 We don't normally add examples to our documentation—it makes
@@ -1002,8 +1008,8 @@ the summary could have avoided swapping elements in the comparison and
 negating the result:
 
 ```swift
-/// Sorts the elements so that `areInOrder(self[i],
-/// self[i+1])` is true for each `i` in `0 ..< length - 2`.
+  /// Sorts the elements so that `areInOrder(self[i],
+  /// self[i+1])` is true for each `i` in `0 ..< length - 2`.
 ```
 
 If we view a strict weak ordering as a generalization of what `<` does, the
@@ -1028,29 +1034,28 @@ Therefore, if we have a sorting implementation that works with any
 strict weak order, we can easily convert it to work with any total
 preorder by passing the predicate through `converseOfComplement`.
 
-
 Note that the name of the predicate became simpler: it no longer tests
 that its arguments represent an _increase_.  Instead, it tells us
 whether the order is correct.  Because the summary is no longer
 tricky, we can drop the example, and we're left with this:
 
 ```swift
-/// Sorts the elements so that `areInOrder(self[i],
-/// self[i+1])` is true for each `i` in `0 ..< length - 2`.
-///
-/// - Precondition: `areInOrder` is a [total
-///   preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
-///   over the elements of `self`.
-/// - Complexity: at most N log N comparisons, where N is the number
-///   of elements.
-mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
+  /// Sorts the elements so that `areInOrder(self[i],
+  /// self[i+1])` is true for each `i` in `0 ..< length - 2`.
+  ///
+  /// - Precondition: `areInOrder` is a [total
+  ///   preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
+  ///   over the elements of `self`.
+  /// - Complexity: at most N log N comparisons, where N is the number
+  ///   of elements.
+  mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
 ```
 
 But we can go further and use a much simpler and more natural summary:
 
 ```swift
-/// Sorts the elements so that all adjacent pairs satisfy
-/// `areInOrder`.
+  /// Sorts the elements so that all adjacent pairs satisfy
+  /// `areInOrder`.
 ```
 
 Usually, the less our documentation looks like code (without
@@ -1081,13 +1086,13 @@ precondition there without overly complicating it, making the final
 declaration:
 
 ```swift
-/// Sorts the elements so that all adjacent pairs satisfy the [total
-/// preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
-/// `areInOrder`.
-///
-/// - Complexity: at most N log N comparisons, where N is the number
-///   of elements.
-mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
+  /// Sorts the elements so that all adjacent pairs satisfy the [total
+  /// preorder](https://en.wikipedia.org/wiki/Weak_ordering#Total_preorders)
+  /// `areInOrder`.
+  ///
+  /// - Complexity: at most N log N comparisons, where N is the number
+  ///   of elements.
+  mutating func sort<T>(areInOrder: (T, T)->Bool) { ... }
 ```
 
 There is one factor we haven't considered in making these changes:
@@ -1103,10 +1108,10 @@ contract is an engineering decision you will have to make. To reduce
 the risk you could add this assertion[^checks], which will stop the program if
 the ordering is strict-weak:
 
-```
-precondition(
-  self.isEmpty || areInOrder(first!, first!),
-  "Total preorder required; did you pass a strict-weak ordering?")
+```swift
+  precondition(
+    self.isEmpty || areInOrder(first!, first!),
+    "Total preorder required; did you pass a strict-weak ordering?")
 ```
 
 [^checks]: See the next chapter for more on checking contracts at
@@ -1155,7 +1160,6 @@ For example,
 > - Document the performance of every operation that doesn't execute in
 >   constant time and space.
 
-
 It is reasonable to put information in the policies without which the
 project's other documentation would be incomplete or confusing, but
 you should be aware that it implies policies *must be read*. We
@@ -1177,7 +1181,7 @@ But suppose you want to change a function's contract? The
 correctness-preserving changes are those that weaken the function's
 preconditions and/or strengthen its postconditions.  For example, this
 method returns the number of steps from the start of a collection to
-an occurence of some value.
+an occurrence of some value.
 
 ```swift
 extension Collection where Element: Equatable {
@@ -1285,7 +1289,7 @@ to promise more efficiency, but never weakened.
 
 ## Polymorphism and Higher-Order Functions
 
-Similar rules apply to the contracts for protocol conformances: a
+Similar rules apply to the contracts for protocol conformance: a
 method satisfying a protocol requirement can have weaker preconditions
 and/or stronger postconditions than required by the protocol:
 

From 95b58623652897c8e0baf0e626fb685d9247565a Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 9 Sep 2025 16:34:31 -0700
Subject: [PATCH 02/12] Removing unnessary math.

---
 better-code/src/chapter-2-contracts.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index ba7f8d6..443320f 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -144,7 +144,7 @@ $S$ establishes **postcondition** $Q$.
 
 For example:
 
-- if we start with $\{$ `x == 2` $\}$ (precondition), after `x += 1`, $\{$ `x == 3` $\}$ (postcondition):
+- if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
   > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
 

From c21f9878a39d060d8465045e1e5ea9c8741ffda8 Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 9 Sep 2025 16:36:21 -0700
Subject: [PATCH 03/12] Consistent spacing.

---
 better-code/src/chapter-2-contracts.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index 443320f..067a9aa 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -152,7 +152,7 @@ For example:
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > $\{$`x < Int.max`$\}$ `x += 1` $\{$`x > Int.min`$\}$
+  > $\{$ `x < Int.max` $\}$ `x += 1` $\{$ `x > Int.min` $\}$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:

From 325cfefa71367408ea0caab77ac7c2ab66da84ed Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 9 Sep 2025 16:43:34 -0700
Subject: [PATCH 04/12] Github markdown wants explicit braces if unbalanced.

---
 better-code/src/chapter-2-contracts.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index 067a9aa..1d04f32 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -135,7 +135,7 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> $\{P\}S\{Q\}$
+> $\lbrace P\rbrace S\lbrace Q\rbrace $
 
 which is an assertion that if **precondition** $P$ is met, operation
 $S$ establishes **postcondition** $Q$.
@@ -146,18 +146,18 @@ For example:
 
 - if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
-  > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
+  > $\lbrace $ `x == 2` $\rbrace $ `x += 1` $\lbrace $ `x == 3` $\rbrace $
 
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > $\{$ `x < Int.max` $\}$ `x += 1` $\{$ `x > Int.min` $\}$
+  > $\lbrace $ `x < Int.max` $\rbrace $ `x += 1` $\lbrace $ `x > Int.min` $\rbrace $
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> $\{P\}S\{Q\} \wedge \{Q\}T\{R\} \Rightarrow \{P\}S;T\{R\}$
+> $\lbrace P\rbrace S\lbrace Q\rbrace  \wedge \lbrace Q\rbrace T\lbrace R\rbrace  \Rightarrow \lbrace P\rbrace S;T\lbrace R\rbrace $
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing
@@ -179,13 +179,13 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-$\{$ `l + m == 0` $\}$ `h = l + m` $\{$ `h <= 0` $\}$. This one isn't particularly
+$\lbrace $ `l + m == 0` $\rbrace $ `h = l + m` $\lbrace $ `h <= 0` $\rbrace $. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- $\{$ `l <= h` $\}$ `let m = (h - l )/2` $\{$ `m >= 0` $\}$, i.e.,
+- $\lbrace $ `l <= h` $\rbrace $ `let m = (h - l )/2` $\lbrace $ `m >= 0` $\rbrace $, i.e.,
 
   ```swift
   // precondition: l <= h
@@ -193,7 +193,7 @@ The following—more useful—triples will help illustrate the sequencing rule:
   // postcondition: m >= 0
   ```
 
-- $\{$ `m >= 0` $\}$ `h = l + m` $\{$ `l <= h` $\}$, i.e.,
+- $\lbrace $ `m >= 0` $\rbrace $ `h = l + m` $\lbrace $ `l <= h` $\rbrace $, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -206,7 +206,7 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-$\{$ `l <= h` $\}$ `let m = (h - l) / 2; h = l + m` $\{$ `l <= h` $\}$, i.e.,
+$\lbrace $ `l <= h` $\rbrace $ `let m = (h - l) / 2; h = l + m` $\lbrace $ `l <= h` $\rbrace $, i.e.,
 
 ```swift
 // precondition: l <= h

From 5bdfb410aab7f94ff81d6fc65bfa7c6827ea9d92 Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 9 Sep 2025 16:46:48 -0700
Subject: [PATCH 05/12] Revert "Github markdown wants explicit braces if
 unbalanced."

This reverts commit 325cfefa71367408ea0caab77ac7c2ab66da84ed.
---
 better-code/src/chapter-2-contracts.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index 1d04f32..067a9aa 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -135,7 +135,7 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> $\lbrace P\rbrace S\lbrace Q\rbrace $
+> $\{P\}S\{Q\}$
 
 which is an assertion that if **precondition** $P$ is met, operation
 $S$ establishes **postcondition** $Q$.
@@ -146,18 +146,18 @@ For example:
 
 - if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
-  > $\lbrace $ `x == 2` $\rbrace $ `x += 1` $\lbrace $ `x == 3` $\rbrace $
+  > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
 
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > $\lbrace $ `x < Int.max` $\rbrace $ `x += 1` $\lbrace $ `x > Int.min` $\rbrace $
+  > $\{$ `x < Int.max` $\}$ `x += 1` $\{$ `x > Int.min` $\}$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> $\lbrace P\rbrace S\lbrace Q\rbrace  \wedge \lbrace Q\rbrace T\lbrace R\rbrace  \Rightarrow \lbrace P\rbrace S;T\lbrace R\rbrace $
+> $\{P\}S\{Q\} \wedge \{Q\}T\{R\} \Rightarrow \{P\}S;T\{R\}$
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing
@@ -179,13 +179,13 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-$\lbrace $ `l + m == 0` $\rbrace $ `h = l + m` $\lbrace $ `h <= 0` $\rbrace $. This one isn't particularly
+$\{$ `l + m == 0` $\}$ `h = l + m` $\{$ `h <= 0` $\}$. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- $\lbrace $ `l <= h` $\rbrace $ `let m = (h - l )/2` $\lbrace $ `m >= 0` $\rbrace $, i.e.,
+- $\{$ `l <= h` $\}$ `let m = (h - l )/2` $\{$ `m >= 0` $\}$, i.e.,
 
   ```swift
   // precondition: l <= h
@@ -193,7 +193,7 @@ The following—more useful—triples will help illustrate the sequencing rule:
   // postcondition: m >= 0
   ```
 
-- $\lbrace $ `m >= 0` $\rbrace $ `h = l + m` $\lbrace $ `l <= h` $\rbrace $, i.e.,
+- $\{$ `m >= 0` $\}$ `h = l + m` $\{$ `l <= h` $\}$, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -206,7 +206,7 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-$\lbrace $ `l <= h` $\rbrace $ `let m = (h - l) / 2; h = l + m` $\lbrace $ `l <= h` $\rbrace $, i.e.,
+$\{$ `l <= h` $\}$ `let m = (h - l) / 2; h = l + m` $\{$ `l <= h` $\}$, i.e.,
 
 ```swift
 // precondition: l <= h

From 742f969facc587eaa9880c36728bdf03f807ae1b Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 9 Sep 2025 16:48:52 -0700
Subject: [PATCH 06/12] Attempt 2 to find compatible syntax for braces.

---
 better-code/src/chapter-2-contracts.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index 067a9aa..f0d7fa1 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -146,13 +146,13 @@ For example:
 
 - if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
-  > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
+  > $\lbrace$ `x == 2` $\rbrace$ `x += 1` $\lbrace$ `x == 3` $\rbrace$
 
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > $\{$ `x < Int.max` $\}$ `x += 1` $\{$ `x > Int.min` $\}$
+  > $\lbrace$ `x < Int.max` $\rbrace$ `x += 1` $\lbrace$ `x > Int.min` $\rbrace$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
@@ -179,13 +179,13 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-$\{$ `l + m == 0` $\}$ `h = l + m` $\{$ `h <= 0` $\}$. This one isn't particularly
+$\lbrace$ `l + m == 0` $\rbrace$ `h = l + m` $\lbrace$ `h <= 0` $\rbrace$. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- $\{$ `l <= h` $\}$ `let m = (h - l )/2` $\{$ `m >= 0` $\}$, i.e.,
+- $\lbrace$ `l <= h` $\rbrace$ `let m = (h - l )/2` $\lbrace$ `m >= 0` $\rbrace$, i.e.,
 
   ```swift
   // precondition: l <= h
@@ -193,7 +193,7 @@ The following—more useful—triples will help illustrate the sequencing rule:
   // postcondition: m >= 0
   ```
 
-- $\{$ `m >= 0` $\}$ `h = l + m` $\{$ `l <= h` $\}$, i.e.,
+- $\lbrace$ `m >= 0` $\rbrace$ `h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -206,7 +206,7 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-$\{$ `l <= h` $\}$ `let m = (h - l) / 2; h = l + m` $\{$ `l <= h` $\}$, i.e.,
+$\lbrace$ `l <= h` $\rbrace$ `let m = (h - l) / 2; h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
 
 ```swift
 // precondition: l <= h

From a5e50d361bb590c45c7a3ad3933f152efa3f8fb2 Mon Sep 17 00:00:00 2001
From: Dave Abrahams <dabrahams@adobe.com>
Date: Thu, 16 Oct 2025 08:51:17 -0700
Subject: [PATCH 07/12] stable=>deterministic, fix cost bound

---
 better-code/src/chapter-2-contracts.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index f0d7fa1..f6c0381 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -949,9 +949,9 @@ function as part of its postconditions, which brings all the
 function's guarantees under one name: its postconditions.
 
 The strict weak ordering requirement is a great example of a
-precondition that can't be efficiently checked.  Even if we could assume the
-comparison is stable, to do so would
-require at least $n^2$ comparisons, where $n$ is the number of
+precondition that can't be checked: there's no way to verify that a function
+is deterministic. Even if we could assume determinism, a complete check
+requires at least $n^3$ comparisons, where $n$ is the number of
 elements, which would violate the complexity bound of the algorithm.
 
 The summary gives the postcondition that no two adjacent elements are

From 249e7f9150abd02a10d8125fd2a64202d5ca5cb2 Mon Sep 17 00:00:00 2001
From: Dave Abrahams <dabrahams@adobe.com>
Date: Thu, 16 Oct 2025 08:51:38 -0700
Subject: [PATCH 08/12] stable=>deterministic

---
 better-code/src/chapter-2-contracts.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index f6c0381..de293fa 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -936,7 +936,7 @@ a meaningful sort with respect to the predicate.  For example, a
 totally unconstrained predicate could return random boolean values,
 and there's no reasonable sense in which the function could be said to
 leave the elements sorted with respect to that.  Therefore the
-predicate at least has to be stable. To leave elements meaningfully
+predicate at least has to be deterministic. To leave elements meaningfully
 sorted, the predicate has to be *transitive*: if it is `true` for
 elements $(i, j)$, it must also be true for elements $(i, j + 1)$.
 A strict weak ordering has both of these properties, among others.

From be5a2f54973d8175a77b6ffdbf51298eb95831bd Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 21 Oct 2025 16:47:00 -0700
Subject: [PATCH 09/12] Update better-code/src/chapter-2-contracts.md

Co-authored-by: Dave Abrahams <dabrahams@adobe.com>
---
 better-code/src/chapter-2-contracts.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index de293fa..dd0a281 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -482,7 +482,7 @@ neither correct nor incorrect; it does something, but does it do the
 
 > All undocumented software is waste. It's a liability for a company.
 >
-> &mdash; Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>)
+> &mdash;Alexander Stepanov (<https://youtu.be/COuHLky7E2Q?t=1773>)
 
 
 Documentation is also essential for local reasoning.  We build atop

From 2bde26579027acb460ecb85acd9a1335c59baf9f Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Tue, 21 Oct 2025 16:52:16 -0700
Subject: [PATCH 10/12] Updating readme with katex instructions and addressing
 PR issues.

---
 README.md                              | 9 ++++++---
 better-code/src/chapter-2-contracts.md | 4 ++--
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 27e4924..903eae9 100644
--- a/README.md
+++ b/README.md
@@ -24,15 +24,18 @@ On Windows, you can download the installer from
 
 Once you have Rust and Cargo installed, you can install or upgrade mdBook by running:
 
+```bash
+cargo install mdbook@0.4.48
+cargo install mdbook-katex
 ```
-cargo install mdbook
-```
+
+The version is currentlypinned to 0.4.48 because that is the version supported by katex
 
 ## Building the book
 
 To build the book, run:
 
-```
+```bash
 mdbook serve ./better-code
 ```
 
diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index b2bf315..85e0bea 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -135,7 +135,7 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> $\{P\}S\{Q\}$
+> $\lbrace P \rbrace S \lbrace Q \rbrace$
 
 which is an assertion that if **precondition** $P$ is met, operation
 $S$ establishes **postcondition** $Q$.
@@ -157,7 +157,7 @@ For example:
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> $\{P\}S\{Q\} \wedge \{Q\}T\{R\} \Rightarrow \{P\}S;T\{R\}$
+> $\lbrace P \rbrace S \lbrace Q \rbrace \wedge \lbrace Q \rbrace T \lbrace R \rbrace \Rightarrow \lbrace P \rbrace S;T \lbrace R \rbrace$
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing

From 00ce55934d8eb1a99ec80db870f031d8712309c0 Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Mon, 22 Dec 2025 20:50:30 -0800
Subject: [PATCH 11/12] Updating katex - cleans up some of the math.

---
 README.md                              | 17 ++++++++++++++---
 better-code/README.md                  | 17 +++++++++++++++--
 better-code/book.toml                  |  3 +--
 better-code/src/chapter-2-contracts.md | 16 ++++++++--------
 4 files changed, 38 insertions(+), 15 deletions(-)

diff --git a/README.md b/README.md
index 903eae9..86df1ce 100644
--- a/README.md
+++ b/README.md
@@ -25,11 +25,22 @@ On Windows, you can download the installer from
 Once you have Rust and Cargo installed, you can install or upgrade mdBook by running:
 
 ```bash
-cargo install mdbook@0.4.48
-cargo install mdbook-katex
+cargo install mdbook
 ```
 
-The version is currentlypinned to 0.4.48 because that is the version supported by katex
+**Install mdbook-katex (for LaTeX math rendering):**
+
+Linux and macOS:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha
+```
+
+Windows:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha --no-default-features --features duktape
+```
+
+Note: On Windows, we use the `duktape` feature instead of the default `quick-js` backend because quick-js doesn't compile on Windows.
 
 ## Building the book
 
diff --git a/better-code/README.md b/better-code/README.md
index f5c7ff2..04e0659 100644
--- a/better-code/README.md
+++ b/better-code/README.md
@@ -19,10 +19,23 @@ Download the installer from [here](https://win.rustup.rs/).
 ### Install mdBook
 
 ```bash
-cargo install mdbook@0.4.48
-cargo install mdbook-katex
+cargo install mdbook
 ```
 
+**Install mdbook-katex (for LaTeX math rendering):**
+
+Linux and macOS:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha
+```
+
+Windows:
+```bash
+cargo install mdbook-katex --version 0.10.0-alpha --no-default-features --features duktape
+```
+
+Note: On Windows, we use the `duktape` feature instead of the default `quick-js` backend because quick-js doesn't compile on Windows.
+
 ### Building and Serving the Book
 
 To build and serve the book locally:
diff --git a/better-code/book.toml b/better-code/book.toml
index 6fab910..8b92e3c 100644
--- a/better-code/book.toml
+++ b/better-code/book.toml
@@ -1,7 +1,6 @@
 [book]
 authors = ["Sean Parent"]
 language = "en"
-multilingual = false
 src = "src"
 title = "Better Code"
 description = "A principled and rigorous approach to software development"
@@ -22,4 +21,4 @@ enable = true
 enable = true
 
 [preprocessor.katex]
-after = ["links"]
+
diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index e26d762..51a0451 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -137,7 +137,7 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> $\lbrace P \rbrace S \lbrace Q \rbrace$
+> $\{ P \} S \{ Q\}$
 
 which is an assertion that if **precondition** $P$ is met, operation
 $S$ establishes **postcondition** $Q$.
@@ -148,18 +148,18 @@ For example:
 
 - if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
-  > $\lbrace$ `x == 2` $\rbrace$ `x += 1` $\lbrace$ `x == 3` $\rbrace$
+  > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
 
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > $\lbrace$ `x < Int.max` $\rbrace$ `x += 1` $\lbrace$ `x > Int.min` $\rbrace$
+  > $\{$ `x < Int.max` $\}$ `x += 1` $\{$ `x > Int.min` $\}$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> $\lbrace P \rbrace S \lbrace Q \rbrace \wedge \lbrace Q \rbrace T \lbrace R \rbrace \Rightarrow \lbrace P \rbrace S;T \lbrace R \rbrace$
+> $\{ P \} S \{ Q \} \wedge \{ Q \} T \{ R \} \Rightarrow \{ P \} S;T \{ R \}$
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing
@@ -181,13 +181,13 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-$\lbrace$ `l + m == 0` $\rbrace$ `h = l + m` $\lbrace$ `h <= 0` $\rbrace$. This one isn't particularly
+$\{$ `l + m == 0` $\}$ `h = l + m` $\{$ `h <= 0` $\}$. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- $\lbrace$ `l <= h` $\rbrace$ `let m = (h - l )/2` $\lbrace$ `m >= 0` $\rbrace$, i.e.,
+- $\{$ `l <= h` $\}$ `let m = (h - l )/2` $\{$ `m >= 0` $\}$, i.e.,
 
   ```swift
   // precondition: l <= h
@@ -195,7 +195,7 @@ The following—more useful—triples will help illustrate the sequencing rule:
   // postcondition: m >= 0
   ```
 
-- $\lbrace$ `m >= 0` $\rbrace$ `h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
+- $\{$ `m >= 0` $\}$ `h = l + m` $\{$ `l <= h` $\}$, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -208,7 +208,7 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-$\lbrace$ `l <= h` $\rbrace$ `let m = (h - l) / 2; h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
+$\{$ `l <= h` $\}$ `let m = (h - l) / 2; h = l + m` $\{$ `l <= h` $\}$, i.e.,
 
 ```swift
 // precondition: l <= h

From afd0b3de9fec31f89fedc672a60818d36e7c677b Mon Sep 17 00:00:00 2001
From: Sean Parent <sean.parent@stlab.cc>
Date: Mon, 22 Dec 2025 20:59:01 -0800
Subject: [PATCH 12/12] Reverting braces - github doesn't like it.

---
 better-code/src/chapter-2-contracts.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/better-code/src/chapter-2-contracts.md b/better-code/src/chapter-2-contracts.md
index 51a0451..e26d762 100644
--- a/better-code/src/chapter-2-contracts.md
+++ b/better-code/src/chapter-2-contracts.md
@@ -137,7 +137,7 @@ terminology.
 
 Hoare used this notation, called a “Hoare triple,”
 
-> $\{ P \} S \{ Q\}$
+> $\lbrace P \rbrace S \lbrace Q \rbrace$
 
 which is an assertion that if **precondition** $P$ is met, operation
 $S$ establishes **postcondition** $Q$.
@@ -148,18 +148,18 @@ For example:
 
 - if we start with `x == 2` (precondition), after `x += 1`, `x == 3` (postcondition):
 
-  > $\{$ `x == 2` $\}$ `x += 1` $\{$ `x == 3` $\}$
+  > $\lbrace$ `x == 2` $\rbrace$ `x += 1` $\lbrace$ `x == 3` $\rbrace$
 
 
 - if `x` is less than the maximum integer (precondition), after `x
   += 1`, `x` is greater than the minimum integer (postcondition):
 
-  > $\{$ `x < Int.max` $\}$ `x += 1` $\{$ `x > Int.min` $\}$
+  > $\lbrace$ `x < Int.max` $\rbrace$ `x += 1` $\lbrace$ `x > Int.min` $\rbrace$
 
 What makes preconditions and postconditions useful for formal proofs
 is this *sequencing rule*:
 
-> $\{ P \} S \{ Q \} \wedge \{ Q \} T \{ R \} \Rightarrow \{ P \} S;T \{ R \}$
+> $\lbrace P \rbrace S \lbrace Q \rbrace \wedge \lbrace Q \rbrace T \lbrace R \rbrace \Rightarrow \lbrace P \rbrace S;T \lbrace R \rbrace$
 
 Given two valid Hoare triples, if the postconditions of the first are
 the preconditions of the second, we can form a new valid triple describing
@@ -181,13 +181,13 @@ h = l + m
 ```
 
 There are many valid Hoare triples for each of them.  For instance,
-$\{$ `l + m == 0` $\}$ `h = l + m` $\{$ `h <= 0` $\}$. This one isn't particularly
+$\lbrace$ `l + m == 0` $\rbrace$ `h = l + m` $\lbrace$ `h <= 0` $\rbrace$. This one isn't particularly
 useful, but it is valid because if `l + m == 0` is true before we
 execute it, `h <= 0` will be true afterwards.
 
 The following—more useful—triples will help illustrate the sequencing rule:
 
-- $\{$ `l <= h` $\}$ `let m = (h - l )/2` $\{$ `m >= 0` $\}$, i.e.,
+- $\lbrace$ `l <= h` $\rbrace$ `let m = (h - l )/2` $\lbrace$ `m >= 0` $\rbrace$, i.e.,
 
   ```swift
   // precondition: l <= h
@@ -195,7 +195,7 @@ The following—more useful—triples will help illustrate the sequencing rule:
   // postcondition: m >= 0
   ```
 
-- $\{$ `m >= 0` $\}$ `h = l + m` $\{$ `l <= h` $\}$, i.e.,
+- $\lbrace$ `m >= 0` $\rbrace$ `h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
 
   ```swift
   // precondition: m >= 0
@@ -208,7 +208,7 @@ precondition means that the operations can be executed in
 sequence, with the sequence having the first precondition and the
 second postcondition. Thus there's a new valid triple:
 
-$\{$ `l <= h` $\}$ `let m = (h - l) / 2; h = l + m` $\{$ `l <= h` $\}$, i.e.,
+$\lbrace$ `l <= h` $\rbrace$ `let m = (h - l) / 2; h = l + m` $\lbrace$ `l <= h` $\rbrace$, i.e.,
 
 ```swift
 // precondition: l <= h