From 33f818642f929f55362661605cb194612b5ddbd8 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 10:32:11 -0700 Subject: [PATCH 1/9] Correct definitions of Lamport properties MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit …and all the consequences of those corrections --- better-code/src/Appendix - Safety.md | 39 +++++++++++++++++++++------- 1 file changed, 30 insertions(+), 9 deletions(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 4d55289..eacdf8b 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -2,10 +2,29 @@ - **Safety** in engineering is the prevention of harm through system design. +- Per [Leslie Lamport's authoritative definitions](https://lamport.azurewebsites.net/tla/safety-liveness.pdf): + - A **behavior** is an infinite sequence of states of some system. We will call a finite sequence of such + - states a **trace**. (You can turn a *trace* into a *behavior* by repeating its final state forever). + + - A **property** is any predicate that applies to behaviors. We will call these **Lamport properties** + since *property* is already such a general term. You can apply a *Lamport property* to a *trace* by first + turning the *trace* into a *behavior* per the previous bullet. + + - A **safety property** is a Lamport property that once violated, cannot be “patched up.” For example, “the + spaceship never left its planned flight path” is a safety property, while “the spaceship is on its planned + flight path” is not, because it could return to the planned flight path after having left it. + + - A **liveness property** is a Lamport property that can potentially eventually be satisfied starting from + any trace. For example, “the spaceship never left its planned flight path” is not a liveness property, + because a trace that violates that property can never be extended to one that satisfies it. Barring the + presence of infinite loops and recursions, “the program has terminated” is a liveness property. + - An **operation** is any executable program or program fragment, from an integer addition to a whole application. - -- A **[safety property](https://en.wikipedia.org/wiki/Safety_and_liveness_properties)** is the *impossibility* of some occurrence *when an operation is used correctly*. For example, this function upholds the safety property that nothing is printed to the console: +- An operation *f* **upholds a Lamport property P iff, given a trace satisfying P whose final state satisfies + the preconditions of *f*, applying *f* produces a trace satisfying P. For example, this function upholds the + safety property that nothing has ever been printed to the console, because given a trace where nothing has been + printed, a legal application of `identity` maintains that property: ```swift /// Returns `x`. @@ -16,9 +35,9 @@ return x } ``` -To be a safety property, it must *compose*. That is, when any two operations *P* and *Q* uphold the property, so does *P* followed by *Q*. For example, freedom from data races is a safety property, but freedom from logical races is not, because when two consecutive non-racy mutations are composed into a larger mutation, another thread can observe the partially mutated state between the two steps. -- A **[liveness property](https://en.wikipedia.org/wiki/Safety_and_liveness_properties)** is the *guarantee* of some occurrence when an operation is used correctly. For example, this function upholds the liveness property that it eventually returns: + And this function upholds the liveness property that the program has terminated, because given a trace where + termination is reachable, a legal application of `identity2` maintains that property: ```swift /// Returns `x`. @@ -30,19 +49,21 @@ To be a safety property, it must *compose*. That is, when any two operations *P } ``` -- An ***X* safe operation** upholds some safety property *X* **even if preconditions are violated**. [^qualification] For example, when `a` is an array, `a[0] = 3` never modifies a variable not mentioned in the expression, even if `a` is empty (which violates the precondition of `a[0]`). We might say that the operation is “expression-mutation safe.” +- The upholding of any Lamport property *composes*. That is, when any two operations *f* and *g* uphold the property, so does *f* followed by *g*. + +- An ***X* safe operation** upholds some safety property *X* **even if preconditions are violated**. [^qualification] For example, when `a` is an array with bounds checking, `a[0] = 3` never modifies a variable not mentioned in the expression, even if `a` is empty (which violates the precondition of `a[0]`). We might say that the operation is “expression-mutation safe.” [^qualification]: note this important distinction—an operation can uphold the memory safety property but not be memory-safe by this definition, because the former depends on preconditions being satisfied but the latter does not. - An ***X* safe language** is one where all primitive operations are *X safe*. It follows that all non-primitive operations—and all possible programs in the language—are *X safe*. A language subset, such as “Swift programs in which no identifier contains the substring `Unsafe` or `unsafe`,” can be considered a language. -- **Memory safety**: the property that invalid memory operations such as out-of-bounds accesses and use-after-free do not occur. +- **Memory safety** is the property that invalid memory operations such as out-of-bounds accesses and use-after-free have not occurred. -- **Type safety**: the property that an instance of one type is never accessed as an instance of another type. +- **Type safety** is the property that an instance of one type has never been accessed as an instance of another type. -- **Thread safety**: the property that a data race does not occur. Sometimes “thread safe” is used to mean that, additionally, deadlock does not occur. Freedom from deadlock can also be viewed as part of a liveness property guaranteeing forward progress. +- **Thread safety** is the property that a data race has never occurred. Sometimes “thread safe” is used to mean that, additionally, deadlock has not occurred. Freedom from deadlock can also be viewed as part of a liveness property guaranteeing forward progress. -- **Data race safety**: the property that a data race does not occur (explicitly excluding freedom from deadlock as a constraint). +- **Data race safety** is the property that a data race does not occur (explicitly excluding freedom from deadlock as a constraint). - **Undefined behavior** is not bounded by any constraints and thus nullifies every safety property. An operation that can have undefined behavior, or a language that includes such an operation, is never *X* safe for any *X*. From 6c57f2e596eb6502e4a9ef03a1d8086ef329a165 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 10:35:13 -0700 Subject: [PATCH 2/9] Delete needless caveats about composability They were not adding anything even before the correction. Fixes #52 --- better-code/src/Appendix - Safety.md | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index eacdf8b..505f5d7 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -80,24 +80,3 @@ - The **safe subset of a safe-by-default language** is a safe language. [^java-data-race]: Some languages, such as Java and JavaScript, define the behavior of data races, but in such a way as to be useless for most programming. - - ----- - -In Lamport’s framework, safety is defined semantically—as a prefix‑closed set of behaviors—but this definition alone does not guarantee compositionality under functional composition. As Abadi and Lamport show in Composing Specifications, and as later clarified by Abadi and Plotkin’s work on refinement‑preserving transformations, safety properties become compositional only when the functions involved are themselves safety‑preserving. In other words, from the fact that a safety property p holds for f(x) and for g(x), nothing follows about p(f(g(x))) unless f and g each preserve p. This distinction—emphasized in surveys such as Freiling and Santen’s work on compositional reasoning—makes clear that prefix‑closure characterizes the semantic nature of safety, while congruence under composition requires an additional structural assumption about the operators acting on behaviors. - -preserving.dvi -https://lamport.org/pubs/abadi-preserving.pdf -lamport.org - - -99583.99626 -https://dlnext.acm.org/doi/pdf/10.1145/99583.99626 -dlnext.acm.org - - -On the Composition of Compositional Reasoning | Springer Nature Link -https://link.springer.com/chapter/10.1007/11786160_8 -link.springer.com - -https://lamport.azurewebsites.net/pubs/abadi-composing.pdf From 3548a2a90f07fff87d706ceefbef7e6feef8e81d Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 10:37:50 -0700 Subject: [PATCH 3/9] Fix formatting --- better-code/src/Appendix - Safety.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 505f5d7..1636684 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -3,8 +3,9 @@ - **Safety** in engineering is the prevention of harm through system design. - Per [Leslie Lamport's authoritative definitions](https://lamport.azurewebsites.net/tla/safety-liveness.pdf): + - A **behavior** is an infinite sequence of states of some system. We will call a finite sequence of such - - states a **trace**. (You can turn a *trace* into a *behavior* by repeating its final state forever). + states a **trace**. (You can turn a *trace* into a *behavior* by repeating its final state forever). - A **property** is any predicate that applies to behaviors. We will call these **Lamport properties** since *property* is already such a general term. You can apply a *Lamport property* to a *trace* by first From 5f4bfbcddf027f624ab5b391044c12970835ca63 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 10:40:23 -0700 Subject: [PATCH 4/9] Note that X-safety composes --- better-code/src/Appendix - Safety.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 1636684..bfe9b8a 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -54,6 +54,8 @@ - An ***X* safe operation** upholds some safety property *X* **even if preconditions are violated**. [^qualification] For example, when `a` is an array with bounds checking, `a[0] = 3` never modifies a variable not mentioned in the expression, even if `a` is empty (which violates the precondition of `a[0]`). We might say that the operation is “expression-mutation safe.” +- Trivially, *X*-safety composes for any *X*. + [^qualification]: note this important distinction—an operation can uphold the memory safety property but not be memory-safe by this definition, because the former depends on preconditions being satisfied but the latter does not. - An ***X* safe language** is one where all primitive operations are *X safe*. It follows that all non-primitive operations—and all possible programs in the language—are *X safe*. A language subset, such as “Swift programs in which no identifier contains the substring `Unsafe` or `unsafe`,” can be considered a language. From 9cf7a707710191d464ca9199f051834da188bd85 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 10:42:16 -0700 Subject: [PATCH 5/9] Improve language --- better-code/src/Appendix - Safety.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index bfe9b8a..1ac1aba 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -52,9 +52,7 @@ - The upholding of any Lamport property *composes*. That is, when any two operations *f* and *g* uphold the property, so does *f* followed by *g*. -- An ***X* safe operation** upholds some safety property *X* **even if preconditions are violated**. [^qualification] For example, when `a` is an array with bounds checking, `a[0] = 3` never modifies a variable not mentioned in the expression, even if `a` is empty (which violates the precondition of `a[0]`). We might say that the operation is “expression-mutation safe.” - -- Trivially, *X*-safety composes for any *X*. +- An ***X* safe operation** upholds some safety property *X* **even if preconditions are violated**. [^qualification] For example, when `a` is an array with bounds checking, `a[0] = 3` never modifies a variable not mentioned in the expression, even if `a` is empty (which violates the precondition of `a[0]`). We might say that the operation is “expression-mutation safe.” The composition of any two *X*-safe operations is *X*-safe. [^qualification]: note this important distinction—an operation can uphold the memory safety property but not be memory-safe by this definition, because the former depends on preconditions being satisfied but the latter does not. From a533193529405fb9423257678a0ffeae9a145607 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 11:12:05 -0700 Subject: [PATCH 6/9] Fix thread safety definition --- better-code/src/Appendix - Safety.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 1ac1aba..1158f59 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -62,9 +62,9 @@ - **Type safety** is the property that an instance of one type has never been accessed as an instance of another type. -- **Thread safety** is the property that a data race has never occurred. Sometimes “thread safe” is used to mean that, additionally, deadlock has not occurred. Freedom from deadlock can also be viewed as part of a liveness property guaranteeing forward progress. +- **Thread safety** is the property that at no point in the trace can another thread cause a data race. Sometimes “thread safe” is used to mean that, additionally, deadlock has not occurred. Freedom from deadlock can also be viewed as part of a liveness property guaranteeing forward progress. -- **Data race safety** is the property that a data race does not occur (explicitly excluding freedom from deadlock as a constraint). +- **Data race safety** is thread safety, but explicitly excluding freedom from deadlock as a constraint. - **Undefined behavior** is not bounded by any constraints and thus nullifies every safety property. An operation that can have undefined behavior, or a language that includes such an operation, is never *X* safe for any *X*. From 2e49200b400794b24c12de623dc886b7d95dc258 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 10 Oct 2026 11:13:38 -0700 Subject: [PATCH 7/9] Markdown fix --- better-code/src/Appendix - Safety.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 1158f59..0f67cdb 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -22,7 +22,7 @@ - An **operation** is any executable program or program fragment, from an integer addition to a whole application. -- An operation *f* **upholds a Lamport property P iff, given a trace satisfying P whose final state satisfies +- An operation *f* **upholds** a Lamport property P iff, given a trace satisfying P whose final state satisfies the preconditions of *f*, applying *f* produces a trace satisfying P. For example, this function upholds the safety property that nothing has ever been printed to the console, because given a trace where nothing has been printed, a legal application of `identity` maintains that property: From 2de0180a185b90a2125f6172b2ab5a6dfb961c71 Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Mon, 19 Oct 2026 14:46:24 -0700 Subject: [PATCH 8/9] Improve examples and symmetry --- better-code/src/Appendix - Safety.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 0f67cdb..04088df 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -12,13 +12,15 @@ turning the *trace* into a *behavior* per the previous bullet. - A **safety property** is a Lamport property that once violated, cannot be “patched up.” For example, “the - spaceship never left its planned flight path” is a safety property, while “the spaceship is on its planned - flight path” is not, because it could return to the planned flight path after having left it. + spaceship is on its planned flight path” is not a safety property, because it could return to the planned + flight path after having left it. “The spaceship never left its planned flight path” is a safety property, + because once the spaceship leaves its planned path, the property is false forever. - A **liveness property** is a Lamport property that can potentially eventually be satisfied starting from - any trace. For example, “the spaceship never left its planned flight path” is not a liveness property, - because a trace that violates that property can never be extended to one that satisfies it. Barring the - presence of infinite loops and recursions, “the program has terminated” is a liveness property. + any trace. For example, “the CPU temperature has always been less than 100 Celsius” is not a liveness + property, because a trace that violates that property can never be extended to one that satisfies it. + ”The CPU temperature is 100 Celsius“ is a liveness property, because no matter the current temperature, + it can become 100 Celsius sometime in the future. - An **operation** is any executable program or program fragment, from an integer addition to a whole application. From 820e1a29ce2a06a28377e7fa2a6d73a67dba0e4a Mon Sep 17 00:00:00 2001 From: Dave Abrahams Date: Sat, 24 Oct 2026 13:31:44 -0700 Subject: [PATCH 9/9] Better liveness text --- better-code/src/Appendix - Safety.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/better-code/src/Appendix - Safety.md b/better-code/src/Appendix - Safety.md index 04088df..a7402d5 100644 --- a/better-code/src/Appendix - Safety.md +++ b/better-code/src/Appendix - Safety.md @@ -16,11 +16,11 @@ flight path after having left it. “The spaceship never left its planned flight path” is a safety property, because once the spaceship leaves its planned path, the property is false forever. - - A **liveness property** is a Lamport property that can potentially eventually be satisfied starting from - any trace. For example, “the CPU temperature has always been less than 100 Celsius” is not a liveness - property, because a trace that violates that property can never be extended to one that satisfies it. - ”The CPU temperature is 100 Celsius“ is a liveness property, because no matter the current temperature, - it can become 100 Celsius sometime in the future. + - A **liveness property** is a Lamport property that can eventually be satisfied starting from + any arbitrary trace. For example, “nothing is printed to the console” is not + a liveness property, because there exist traces (those that have printed to the console) that + cannot be extended to satisfy it. “"Hello, world" is printed to the console” is a liveness + property, because no matter what has come before, the program can print “Hello, world”. - An **operation** is any executable program or program fragment, from an integer addition to a whole application. @@ -39,7 +39,7 @@ } ``` - And this function upholds the liveness property that the program has terminated, because given a trace where + And this function upholds the liveness property that the program terminates, because given a trace where termination is reachable, a legal application of `identity2` maintains that property: ```swift @@ -52,7 +52,8 @@ } ``` -- The upholding of any Lamport property *composes*. That is, when any two operations *f* and *g* uphold the property, so does *f* followed by *g*. +- The upholding of any Lamport property *composes*. That is, when any two operations *f* and *g* uphold the property, + so does *f* followed by *g*. - An ***X* safe operation** upholds some safety property *X* **even if preconditions are violated**. [^qualification] For example, when `a` is an array with bounds checking, `a[0] = 3` never modifies a variable not mentioned in the expression, even if `a` is empty (which violates the precondition of `a[0]`). We might say that the operation is “expression-mutation safe.” The composition of any two *X*-safe operations is *X*-safe.