Merge branch 'main' into chapter-2-combined

src/SUMMARY.md

@@ -3,20 +3,19 @@
 [Overview](./overview.md)
 
 # The basics
-- [Introduction](./intro.md)
-- [Installation](./install.md)
-- [Getting started](./getting-started.md)
+- [Introduction]()
+- [Installation]()
+<!-- - [Getting started]() -->
 - [Basic specifications](./basic-specs.md)
-  - [`assert` and `assume`](./assert-assume.md)
-  - [requires, ensures, and preserves](./requires-ensures.md)
-- [Ghost Code and Pure Functions](./basic-ghost-pure.md)
+  <!-- - [`assert` and `assume`](./assert-assume.md) -->
+  <!-- - [requires, ensures, and preserves](./requires-ensures.md)-->
 - [Array Operations](./basic-array.md)
-- [Overflow Checking](./overflow.md)
 - [Loops](./loops.md)
   - [Invariants](./loops-invariant.md)
   - [Binary Search](./loops-binarysearch.md)
   - [Range](./loops-range.md)
-- [Ghost code](./ghost.md)
+- [Overflow Checking](./overflow.md)
+- [Ghost Code and Pure Functions](./basic-ghost-pure.md)
 
 # Reasoning about Memory Accesses with Permissions
 - [Permission to write](./permission-write.md)

src/overview.md

@@ -1 +1,14 @@
 # Overview
+
+<div class="warning">
+🚧 This book is under construction. Thus, it is very incomplete at the moment and it is likely to change significantly. 🚧
+</div>
+
+This book is an online resource that teaches how to prove the correctness of your programs written in Go against a formal specification.
+We use the [Gobra](https://www.pm.inf.ethz.ch/research/gobra.html) verifier, and we exemplify it on multiple examples and exercises.
+
+If you find errors or have suggestions, please file an issue [here](https://github.com/viperproject/gobra-book/issues).
+
+If you are interested in contributing directly to the project, please refer to our [guide for contributors](https://github.com/viperproject/gobra-book/blob/main/CONTRIBUTING.md).
+
+