minor grammar changes.

src/common-programming-concepts/functions.md

@@ -50,6 +50,8 @@ A function body is a sequence of statements enclosed in curly braces `{}`.
 
 Methods are declared **inside the struct body**, after the field list. Instance methods take `self` (or `mut self`) as the first parameter. Associated functions omit `self` and are called with `::`.
 
+In the code example below, the **v** tab shows the Rocq translation of the Inference code, which is used for formal verification.
+
 <div class="ifc-tabs">
 <div class="ifc-tab-bar">
 <button class="ifc-tab active">inf</button>

src/getting-started/hello-world.md

@@ -46,6 +46,16 @@ On Windows:
 
 The compiler will generate a WebAssembly binary module at `out/hello_world.wasm`.
 
+## Formal Verification and Rocq
+
+A unique feature of the Inference programming language is its focus on *formal verification*. This means you can mathematically prove that your code is correct and follows its specification.
+
+To support this, the compiler can translate your Inference code into **Rocq** (formerly known as Coq), a powerful interactive theorem prover. These translations are stored in files with a `.v` extension.
+
+While you do not need to know Rocq to write and run Inference programs, you will see `.v` files and Rocq translations mentioned throughout this book. Many code examples include a **v** tab that shows how the code is represented for the theorem prover.
+
+For more information on how to generate and use these files, see [Appendix D - Compilation modes](../appendix/d-infs-reference.md#compilation-modes).
+
 > [!Note]
 > You can also use the `infc` compiler directly as an alternative:
 >

src/introduction.md

@@ -8,7 +8,7 @@ The key power of Inference is that it has formal verification built-in from the
 
 ### Developer Teams
 
-Inference provides a way to rigorously ensure the correctness of code through formal verification. For development teams working on mission-critical applications, this means they can obtain mathematical guarantees that specified properties of their programs always hold, rather than relying solely on testing and code review. This leads to substantially lower residual defect risk, higher quality software, increased reliability, and improved safety of its users.
+Inference provides a way to rigorously ensure the correctness of code through formal verification. Development teams working on mission-critical applications can obtain mathematical guarantees that specified properties of their programs always hold, rather than relying solely on testing and code review. This leads to substantially lower residual defect risk, higher quality software, increased reliability, and improved safety of its users.
 
 Examples of such software include, but are not limited to:
 - Cryptographic software and security systems

src/non-determinism/uzumaki.md

@@ -8,7 +8,7 @@ The expression `@` (read *uzumaki*) is a value attribute that represents **every
 error[A006]: uzumaki (@) is only valid inside a non-deterministic block
 ```
 
-## A minimal use
+## A minimal example
 
 Below, `square` is the executable function we want to reason about. `SquareProps` is a `spec` block whose single property claims that for every `i32` value of `x`, `square(x)` is at least zero. `let x: i32 = @;` binds `x` to the whole `i32` domain; the surrounding `forall` requires the final `assert` to hold for every one of those values — except those the inner `assume` filters out.