use soundness in explaining the safety invariant

Author: RalfJung

Diff for: reference/src/glossary.md

@@ -129,7 +129,7 @@ fn main() { unsafe {
 The *safety* invariant is an invariant that safe code may assume all data to uphold.
 This invariant is used to justify which operations safe code can perform.
 The safety invariant can be temporarily violated by unsafe code, but must always be upheld when interfacing with unknown safe code.
-It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* can be used by safe code to *cause* UB.
+It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* is [sound][soundness]
 
 In terms of code, some data computed by `TERM` (possibly constructed from some `arguments` that can be *assumed* to satisfy the safety invariant) is valid at type `T` if and only if the following library function can be safely exposed to arbitrary (safe) code as part of the public library interface:
 ```rust,ignore
@@ -147,6 +147,7 @@ To summarize: *Data must always be valid, but it only must be safe in safe code.
 For some more information, see [this blog post](https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html).
 
 #### Soundness (of code / of a library)
+[soundness]: #soundness-of-code--of-a-library
 
 We say that a library (or an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API.
 Conversely, the library/function is *unsound* if safe code *can* cause Undefined Behavior.